// ************************************************************************** // // eses eses // eses eses // eses eseses esesese eses Embedded Systems Group // ese ese ese ese ese // ese eseseses eseseses ese Department of Computer Science // eses eses ese eses // eses eseses eseseses eses University of Kaiserslautern // eses eses // // ************************************************************************** module Presburger( int x, y, z ) { nothing; } satisfies { // --- " <= " is a total order ord01 : assert x <= x; ord02 : assert x<=y & y<=x -> x==y; ord03 : assert (x <= y) & (y <= z) -> (x <= z); ord04 : assert (x <= y) | (y <= x); // --- "<" is a strict total order ord05 : assert !(x < x); ord06 : assert (x < y) -> !(y < x); ord07 : assert (x < y) & (y < z) -> (x<z); ord08 : assert (x < y) | (x==y) | (y<x); // --- defining numeric relations by "<" ord09 : assert (x <= y) <-> (x<y) | (x==y); ord10 : assert (x>y) <-> (y<x); ord11 : assert (x>=y) <-> !(x<y); ord12 : assert (x==y) <-> !(x<y) & !(y<x); // --- defining numeric relations by " <= " ord13 : assert (x<y) <-> (x <= y) & !(y <= x); ord14 : assert (x>y) <-> !(x <= y); ord15 : assert (x>=y) <-> (y <= x); ord16 : assert (x==y) <-> (x <= y) & (y <= x); // --- ring axioms --------------------- r01 : assert x+0==x; r02 : assert x+y==y+x; r03 : assert (x+y)+z == x+(y+z); r04 : assert x+(0-x)==0; // --- arithmetic laws --------------------- arith00 : assert x*0==0; arith01 : assert (x+y)-x==y; arith03 : assert x-(y+z) == x-y-z; arith04 : assert 1*x == x; arith05 : assert 2*x == x+x; arith06 : assert 3*x == x+x+x; // --- monotonicity ------------------------ mono00 : assert (x==y) <-> (x+z==y+z); mono01 : assert (x <= y) <-> (x+z <= y+z); mono02 : assert (x<y) <-> (x+z<y+z); mono03 : assert (x+y==0) & (0 <= x) & (0 <= y) -> (x==0) & (y==0); mono04 : assert (x+y==x) -> (y==0); mono05 : assert (x<y) & (0 <= z) -> (x<y+z); mono06 : assert (x<y) & (y <= z) -> (x<z); // --- other stuff ------------------------ div2 : assert exists y:int. ((x == y+y) | (x == y+y+1)); div3 : assert exists y:int. ((x == y+y+y) | (x == y+y+y+1) | (x == y+y+y+2)); div4 : assert exists y:int. ((x == y+y+y+y) | (x == y+y+y+y+1) | (x == y+y+y+y+2) | (x == y+y+y+y+3)); div5 : assert exists y:int. ((x == y+y+y+y+y) | (x == y+y+y+y+y+1) | (x == y+y+y+y+y+2) | (x == y+y+y+y+y+3) | (x == y+y+y+y+y+4)); unbounded : assert exists y:int. (x<y); }