Bigtoe Interactive
Demo
The Ocaml source of Bigtoe: bigtoe.tar.gz
- to clean: make clean
- to build: make
Numerical Expression Language Boolean Expression Language
expr::= var exprb::= TT
integer expr == expr
expr + expr expr <= expr
expr - expr expr < expr
expr * expr expr >= expr
expr > expr
exprb /\ exprb
exprb \/ exprb
! exprb
Spatial Assertion Assertion Language
sigma ::= E Assrt ::= (exprb | sigma)
expr |->_ Assert \/ Assert
expr |-> expr
list expr expr
Programming Language Goals
Programming Language (cmd): var := expr (alternative: var <- expr) Goal : { assert } cmd { assert }
var := [expr] (alternative: var <-* expr) assert |- assert
[expr] := expr (alternative: expr *<- expr) exprb
if (exprb) then { cmd } else { cmd }
while (exprb) [assert] { cmd }
cmd; cmd
Example of program:
{TT | list i 0}
j <- 0;
while (i <> 0) [(TT | list i 0 ** list j 0)]{
k <-* i;
i *<- j;
j <- i;
i <- k
}
{TT | list j 0}
{TT | list i 0}
j := i;
while (j <> 0) [
(TT | list i j ** list j 0)
] {
j := [j]
}
{TT | list i 0}
{TT | list i 0 ** list j 0}
if (i == 0) then {
i := j
} else {
curr := i;
tmp := [curr];
while (tmp <> 0)
[(TT | list i curr ** curr |-> tmp ** curr + 1 |->_ ** list tmp 0 ** list j 0)]{
curr := tmp;
tmp := [curr]
};
[curr] := j
}
{TT | list i 0}
{TT | x |->
vx ** x+1 |->_ ** list y 0}
[x] := y
{TT | list x 0}
{x <> 0 | list i 0 ** x |->_ ** x + 1 |-> data}
x *<- 0;
if (i == 0){
i <- x
} else {
curr <- i;
tmp <-* curr;
while (tmp <> 0)
[{i <> 0 | list i curr ** curr |-> tmp ** curr + 1 |->_ ** list tmp 0 ** x |-> 0 ** x + 1 |-> data}]{
curr <- tmp;
tmp <-* curr
};
curr *<- x
}
{TT | list i x ** x |-> 0 ** x + 1 |-> data}