Commit d2cc224b authored by Andrei Paskevich's avatar Andrei Paskevich

add a type invariant for arrays and strings

parent e12880ca
......@@ -98,7 +98,7 @@ module BinarySearchInt32
exception Not_found (* raised to signal a search failure *)
let binary_search (a : array int) (v : int)
requires { 0 <= length a <= max_int }
requires { length a <= max_int }
requires { forall i1 i2 : int. 0 <= i1 <= i2 < length a -> a[i1] <= a[i2] }
ensures { 0 <= result < length a /\ a[result] = v }
raises { Not_found -> forall i:int. 0 <= i < length a -> a[i] <> v }
......
......@@ -63,7 +63,7 @@ module CountingSort
(* sorts array a into array b *)
let counting_sort (a: array int) (b: array int)
requires { k_values a /\ 0 <= length a = length b }
requires { k_values a /\ length a = length b }
ensures { sorted b /\ permut a b }
= let c = make k 0 in
for i = 0 to length a - 1 do
......@@ -100,7 +100,7 @@ module InPlaceCountingSort
(* sorts array a in place *)
let in_place_counting_sort (a: array int)
requires { k_values a /\ 0 <= length a }
requires { k_values a }
ensures { sorted a /\ permut (old a) a }
= 'L:
let c = make k 0 in
......
......@@ -137,7 +137,6 @@ module EditDistance
(* The program. *)
let distance (w1: array char) (w2: array char)
requires { length w1 >= 0 /\ length w2 >= 0 }
ensures { min_dist (word_of w1) (word_of w2) result }
= let n1 = length w1 in
let n2 = length w2 in
......
......@@ -23,7 +23,6 @@ module Flag
end
let dutch_flag (a:array color) : unit
requires { 0 <= length a }
ensures { exists b r: int.
monochrome a 0 b Blue /\
monochrome a b r White /\
......
......@@ -123,7 +123,7 @@ module KnuthMorrisPratt
(forall k: int. 0 <= k < r -> not (matches a k p 0 (length p)))
let kmp (p a: array char)
requires { 1 <= length p /\ 0 <= length a }
requires { 1 <= length p }
ensures { first_occur p a result }
= let m = length p in
let n = length a in
......
......@@ -328,7 +328,6 @@ let select (s:suffixArray) (i:int) : int
= s.suffixes[i]
let create (a:array int) : suffixArray
requires { a.length >= 0 }
ensures { result.values = a /\ inv result }
=
let n = a.length in
......
......@@ -19,7 +19,7 @@ module InvertingAnInjection
predicate range (a: array int) (n: int) = M.range a.elts n
let inverting (a: array int) (b: array int) (n: int)
requires { 0 <= n = length a = length b /\ injective a n /\ range a n }
requires { n = length a = length b /\ injective a n /\ range a n }
ensures { injective b n }
= for i = 0 to n - 1 do
invariant { forall j: int. 0 <= j < i -> b[a[j]] = j }
......@@ -29,7 +29,7 @@ module InvertingAnInjection
(* variant where array b is returned /\ with additional post *)
let inverting2 (a: array int) (n: int)
requires { 0 <= n = length a /\ injective a n /\ range a n }
requires { n = length a /\ injective a n /\ range a n }
ensures { length result = n /\ injective result n /\
forall i: int. 0 <= i < n -> result[a[i]] = i }
= let b = make n 0 in
......
......@@ -13,7 +13,7 @@ module MaxAndSum
use import array.Array
let max_sum (a: array int) (n: int)
requires { 0 <= n = length a /\ forall i:int. 0 <= i < n -> a[i] >= 0 }
requires { n = length a /\ forall i:int. 0 <= i < n -> a[i] >= 0 }
ensures { let (sum, max) = result in sum <= n * max }
= let sum = ref 0 in
let max = ref 0 in
......@@ -39,7 +39,7 @@ module MaxAndSum2
(l < h && exists k: int. l <= k < h && m = a[k]))
let max_sum (a: array int) (n: int)
requires { 0 <= n = length a /\ forall i:int. 0 <= i < n -> a[i] >= 0 }
requires { n = length a /\ forall i:int. 0 <= i < n -> a[i] >= 0 }
ensures { let (s, m) = result in s = sum a 0 n /\ is_max a 0 n m /\ s <= n * m }
= let s = ref 0 in
let m = ref 0 in
......
......@@ -95,7 +95,7 @@ module NQueens
done
let queens (board: array int) (n: int)
requires { 0 <= length board = n }
requires { length board = n }
ensures { forall b:array int. length b = n -> is_board b n -> not (solution b n) }
raises { Solution -> solution board n }
= bt_queens board n 0
......
......@@ -13,6 +13,7 @@ module Array
use import map.Map as M
type array 'a model { length : int; mutable elts : map int 'a }
invariant { 0 <= self.length }
function get (a: array 'a) (i: int) : 'a = M.get a.elts i
......@@ -61,7 +62,7 @@ module Array
forall i:int. 0 <= i < length a2 -> result[length a1 + i] = a2[i] }
val sub (a: array 'a) (ofs: int) (len: int) : array 'a
requires { 0 <= ofs /\ ofs + len <= length a }
requires { 0 <= ofs /\ 0 <= len /\ ofs + len <= length a }
ensures { length result = len }
ensures { forall i:int. 0 <= i < len -> result[i] = a[ofs + i] }
......@@ -70,7 +71,7 @@ module Array
ensures { forall i:int. 0 <= i < length result -> result[i] = a[i] }
let fill (a: array 'a) (ofs: int) (len: int) (v: 'a)
requires { 0 <= ofs /\ ofs + len <= length a }
requires { 0 <= ofs /\ 0 <= len /\ ofs + len <= length a }
ensures { forall i:int.
(0 <= i < ofs \/ ofs + len <= i < length a) -> a[i] = (old a)[i] }
ensures { forall i:int. ofs <= i < ofs + len -> a[i] = v }
......@@ -84,8 +85,8 @@ module Array
val blit (a1: array 'a) (ofs1: int)
(a2: array 'a) (ofs2: int) (len: int) : unit writes {a2}
requires { 0 <= ofs1 /\ ofs1 + len <= length a1 }
requires { 0 <= ofs2 /\ ofs2 + len <= length a2 }
requires { 0 <= ofs1 /\ 0 <= len /\ ofs1 + len <= length a1 }
requires { 0 <= ofs2 /\ ofs2 + len <= length a2 }
ensures { forall i:int.
(0 <= i < ofs2 \/ ofs2 + len <= i < length a2) -> a2[i] = (old a2)[i] }
ensures { forall i:int.
......
......@@ -53,6 +53,7 @@ module String
use import map.Map as M
type string model { length: int; mutable chars: map int char }
invariant { self.length >= 0 }
val create (len:int) : string
requires { len >= 0 } ensures { length result = len }
......@@ -117,6 +118,7 @@ module Buffer
use import map.Map as M
type t model { mutable length: int; mutable contents: map int char }
invariant { self.length >= 0 }
val create (size:int) : t
requires { size >= 0 } ensures { result.length = 0 }
......
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