Commit 19b6b500 authored by Andrei Paskevich's avatar Andrei Paskevich

convert some library modules in mach/

parent 5b8ef5f2
...@@ -37,7 +37,7 @@ end ...@@ -37,7 +37,7 @@ end
module Bounded_int module Bounded_int
use export int.Int use import int.Int
type t type t
...@@ -62,7 +62,7 @@ module Bounded_int ...@@ -62,7 +62,7 @@ module Bounded_int
requires { "expl:integer overflow" in_bounds (to_int a - to_int b) } requires { "expl:integer overflow" in_bounds (to_int a - to_int b) }
ensures { to_int result = to_int a - to_int b } ensures { to_int result = to_int a - to_int b }
val ( *) (a:t) (b:t) : t val (*) (a:t) (b:t) : t
requires { "expl:integer overflow" in_bounds (to_int a * to_int b) } requires { "expl:integer overflow" in_bounds (to_int a * to_int b) }
ensures { to_int result = to_int a * to_int b } ensures { to_int result = to_int a * to_int b }
......
...@@ -5,7 +5,7 @@ module OneTime ...@@ -5,7 +5,7 @@ module OneTime
use import int.Int use import int.Int
type t model { v: int; mutable ghost valid: bool } type t = abstract { v: int; mutable valid: bool }
val to_int (x: t) : int val to_int (x: t) : int
ensures { result = x.v } ensures { result = x.v }
......
...@@ -5,7 +5,7 @@ module Peano ...@@ -5,7 +5,7 @@ module Peano
use import int.Int use import int.Int
type t model { v: int } type t = abstract { v: int }
val to_int (x: t) : int val to_int (x: t) : int
ensures { result = x.v } ensures { result = x.v }
......
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