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

• Reverse list:

		{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}

• List traversal:
  

		{TT | list i 0}
		j := i;
		while (j <> 0) [
		         (TT | list i j ** list j 0)
		        ] {
        
		        j := [j]
        
		}
		{TT | list i 0}   

• List append:
  

		{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}

• Insert (head):

• Insert (tail):
  

		{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}