HCL (Hoare Command Language) is a programming language that aims to provide a framework to explore ideas related to formal methods for software, software verification, and program derivation. Based on the ideas of Dijkstra, Hoare, and Dahl. HCL is an extended compiler for the Disjktra's GCL program definition language. It is composed of a virtual machine (VHCL), and the compiler that generates VM code. The later is where the semantics and verification procedures resides. The former translates an HCL program, to a VHCL file with the same semantics as the original file. Having a virtual machine allow us to take memory snapshots that serves as a material for a rigorous verification that the program does meet an specification.
The main goals of HCL are:
- Provide a computer language to express ideas written in GCL (Guarded Command Language), and understand the basics of axiomatic semantics.
- Serve as a research canvas about novel verification schemes using a well-defined and a manageable programming language as a basis.
## Why does HCL exists?
Axiomatic semantics, Hoare-Floyd logic, and Dijkstra's ideas for structured programming and program derivation and specification, are sometimes viewed as impractical and old standards for software engineering. Conversely to that, we do think, that those ideas provide a basis to rigorous software engineering without the need of fancy tools, but providing programmers with a mental abstraction to reason about pieces of code.
Real programming languages, does not provide standard libraries to reason about software or complex assertion predicates. The focus of the popular programming languages, is to give a tool to develop real software; thinking about software does not goes well with real software engineering. HCL is a simple, small but yet powerful tool to reason about simple programs; the same programs that we all learnt about while we're learning to program a computer.
HCL has two parts, the compiler, and the VM code interpreter. The compiler job is to generate files that the VM interpreter can understand preserving the semantics of both the verification commands, and the code. The job of the VM interpreter is to check whether or not the program meets the specification and at the same time, run the code.
The following program, reads a number, and prints the fibonacci numbers up to fib(n). The following figures shows both the code written in HCL and the compiled version to be interpreted by the VM.
program fibonacci
begin
var f0, f1, ft, n, i : int
var newline : char
newline ← "\n"
read(n)
print newline
f0, f1, i, ft ← 0, 1, 0, 0
do i < n →
ft ← f0 + f1
f0, f1 ← f1, ft
i ← i + 1
print f0
print newline
od
end;; fibonacci.vhcl : Autogenerated file by HCL Compiler v1.0
;; Auxiliar character defintion
;; Space character
set _sysspace char
;; New Line character
set _sysnl char
;; Space character initialization
mov _sysspace 100000
;; New Line character initialization
mov _sysnl 001010
;; General variable defintion
set f00 integer
set f10 integer
set ft0 integer
set i0 integer
set newline0 char
set n0 integer
;; General program execution routine
mov newline0 _sysnl
readint n0
print newline0
mov f00 0
mov f10 1
mov i0 0
mov ft0 0
do:
gss _do0guard0
clc:
cmp i0 n0
slt:
mov .r4int 1
geq:
mov .r4int 0
mov _do0guard0 .r4int
act _do0guard0:
mov .r3int f00
add .r3int f10
mov ft0 .r3int
mov f00 f10
mov f10 ft0
mov .r3chr i0
add .r3chr 1
mov i0 .r3chr
print f00
print newline0
halt