updated examples/bts

parent 02be08fa
......@@ -2,7 +2,7 @@ module M
use import int.Int
let f ()
ensures { let (a,b,c) = result in a > 0 }
ensures { let (a,_b,_c) = result in a > 0 }
=
(1,2,3)
end
......
......@@ -10,7 +10,7 @@ theory Signed
predicate in_range (x : int) =
(first <= x <= last)
function to_int (n : signed_type) : int
val function to_int (n : signed_type) : int
function from_int (n : int) : signed_type
......
......@@ -6,7 +6,7 @@ module M
type t = A | B
type s = { field1 : t -> t ; field2 : t -> t }
function const (x:'b) : 'a -> 'b = \_:'a.x
function const (x:'b) : 'a -> 'b = fun _ -> x
predicate p (u:s) (a b:t) = u.field1 = const a /\ u.field2 = const b
......
theory T
namespace A
scope A
goal g:true
end
namespace B
scope B
goal g:false
end
......@@ -18,11 +18,11 @@ module A
predicate q
namespace B
scope B
let f () : unit ensures { p } = ()
end
namespace C
scope C
let f () : unit ensures { q <-> p } = ()
end
......
......@@ -6,7 +6,7 @@ module M
val x : ref int
let f () : int
let f () : int
ensures { result = !x }
= !x
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment