Skip to content

Latest commit

 

History

History
95 lines (80 loc) · 1.5 KB

README.md

File metadata and controls

95 lines (80 loc) · 1.5 KB
Raw

Hoare Logic

Sample Code

  • There can be only 26 variables(int and bool - a to z). Any type of assignment is possible after declaration only
  • There are 26 integer arrays - A to Z
  • Two dataypes int and bool
  • pre stands for precondition. post for post condition and inv for loop invariant
  • @ stands for universal quantifier and # stands for existensial quantifier
  • Datatypes of free variables need to be mentioned. Arrays are already of int type

Installation

Install z3 solver

make
./a.out < tests/copy.txt

Valid Hoare Triples

pre true;
A[0] = 1;
post A[0]==1;

pre {
	int n;
	n>0;
}
n=5;
A[3] = n;
post A[3] == 5;

pre {
	int x;
	int y;
	(x>0) && (y>0)&& (x>=y);
}

int r;
r = x;

inv (x>0) && (y>0)&& (x>=y) && (r>=0) && (r<=x);
while(r>=y){
 	r = r - y;
}

post (x>0) && (y>0)&& (x>=y) && (r>=0) && (r<y) && (r>=0) && (r<=x);

pre {
	int x;
	(x>0); 
}

if (x%2 == 0){
	x = x+1;
}
else {
	x = x+2;
}

post x%2 == 1;

Invalid Hoare triples

pre true;
A[0] = 1;
post A[0]==2;

pre {
	int i;
	i<0;
}
post i>0;

Check tests for more examples.

Output

  • Proves the correctness of hoare-triple. Provides counter-example if fails.

Reference