Commit 4e71025c authored by Guillaume Melquiond's avatar Guillaume Melquiond

Fix some examples.

parent d50aedb7
......@@ -70,7 +70,11 @@ module InsertionSortGen
use import array.ArrayPermut
use import array.ArrayEq
clone import map.MapSorted as M
type elt
val predicate le elt elt
clone import map.MapSorted as M with type elt = elt, predicate le = le
axiom le_refl: forall x:elt. le x x
......
......@@ -53,7 +53,11 @@ module InsertionSortNaiveGen
use import array.Array
use import array.ArrayPermut
clone import map.MapSorted as M
type elt
val predicate le elt elt
clone import map.MapSorted as M with type elt = elt, predicate le = le
axiom le_refl: forall x:elt. le x x
......@@ -111,7 +115,7 @@ module InsertionSortParam
type elt
predicate le param elt elt
val predicate le param elt elt
axiom le_refl: forall p:param, x:elt. le p x x
......@@ -172,7 +176,7 @@ module InsertionSortParamBad
type elt
predicate le param elt elt
val predicate le param elt elt
axiom le_refl: forall p:param, x:elt. le p x x
......
......@@ -245,8 +245,8 @@ module Balance
use import ref.Ref
(** we assume that any rope length is smaller than fib (max+1) *)
constant max : int (* e.g. = 100 *)
axiom max_at_least_2: 2 <= max
val constant max : int (* e.g. = 100 *)
ensures { 2 <= result }
function string_of_array (q: Array.array rope) (l u: int) : string
(** q[u-1] + q[u-2] + ... + q[l] *)
......
......@@ -148,17 +148,18 @@ end
module NQueens63
use import int.Int
use import ref.Refint
use import mach.array.Array63
use import mach.int.Int63
predicate is_board (board: array63 int63) (pos: int) =
predicate is_board (board: array int63) (pos: int) =
forall q: int. 0 <= q < pos ->
0 <= to_int board[q] < to_int (length board)
exception MInconsistent
let check_is_consistent (board: array63 int63) (pos: int63)
let check_is_consistent (board: array int63) (pos: int63)
requires { 0 <= to_int pos < to_int (length board) }
requires { is_board board (to_int pos + 1) }
= try
......@@ -182,7 +183,7 @@ module NQueens63
use mach.peano.Peano as P
let rec count_bt_queens
(solutions: ref P.t) (board: array63 int63) (n: int63) (pos: int63)
(solutions: ref P.t) (board: array int63) (n: int63) (pos: int63)
requires { to_int (length board) = to_int n }
requires { 0 <= to_int pos <= to_int n }
requires { is_board board (to_int pos) }
......
......@@ -92,6 +92,10 @@ module Array
ensures { forall i:int.
ofs2 <= i < ofs2 + len -> a[i] = old a[ofs1 + i - ofs2] }
val ghost function ([<-]) (a: array 'a) (i: int) (v: 'a): array 'a
ensures { result.length = a.length }
ensures { result.elts = a.elts[i <- v] }
(*** TODO?
- concat : 'a array list -> 'a array
- to_list
......
......@@ -80,6 +80,9 @@ module Bounded_int
axiom extensionality: forall x y: t. to_int x = to_int y -> x = y
val (=) (a:t) (b:t) : bool
ensures { result <-> to_int a = to_int b }
val (<=) (a:t) (b:t) : bool
ensures { result <-> to_int a <= to_int b }
......
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