// ************************************************************************** // // 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 // // ************************************************************************** // This file demonstrates the theorem proving facilities of Averest // concerning bitvectors. // ************************************************************************** macro range = 16; module SignedBitArithmetic(int{range} x,y,z) { nothing; } satisfies { // --- " <= " is a total order ord00 : assert (-range <= x) & (x < range); 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); // --- field axioms --------------------- f01 : assert x + +0 == x; f02 : assert x + y == y + x; f03 : assert (x + y) + z == x + (y + z); f04 : assert x + (+0 - x) == +0; f05 : assert x * +0 == +0; f06 : assert x == x * +1; f07 : assert x * y == y * x; f08 : assert x * (y * z) == (x * y) * z; f09 : assert x * (y + z) == x * y + x * z; // --- monotonicity ------------------------ mono00: assert (x == y) <-> (x + z == y + z); mono01[DisProveA]: assert (x <= y) <-> (x + z <= y + z); // counterexample for mono01: assert x == 0000, y=1000, z=1000 mono02[DisProveA]: assert (x < y) <-> (x + z < y + z); // counterexample for mono02: assert x == 0000, y=1000, z=1000 mono03: assert (x + y == +0) & (+0 <= x) & (+0 <= y) -> (x == +0) & (y == +0); mono04: assert (x + y == x) -> (y == +0); mono05[DisProveA]: assert (x < y) & (+0 <= z) -> (x < y+z); // counterexample for mono05: assert x == 0000, y=0100, z=0100 mono06: assert (x < y) & (y <= z) -> (x < z); // --- division ------------------------ div1 : assert !(y == +0) -> (+0 <= x % y); div2 : assert (+0 < y) -> (x % y < y); div3 : assert (y < +0) -> (y < x % y); div4 : assert (y!=+0) -> (x == (x / y) * y + (x % y)); }