Bigtoe Interactive Demo

The Ocaml source of Bigtoe: bigtoe.tar.gz


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}