 ### Commit some more examples.

parent b7d720e3
 ... ... @@ -40,8 +40,8 @@ input sequence. module PigeonHole (** The Why standard library provides a lemma [map.MapInjection.injective_surjective] stating that a map from [(0..n-1)] to [(0..n-1)] that is an injection is also a `map.MapInjection.injective_surjective` stating that a map from `(0..n-1)` to `(0..n-1)` that is an injection is also a surjection. This is more or less equivalent to the pigeon-hole lemma. However, we need such a lemma more generally on functions instead of maps. ... ... @@ -54,13 +54,13 @@ module PigeonHole predicate range (f: int -> int) (n: int) (m:int) = forall i: int. 0 <= i < n -> 0 <= f i < m (** [range f n m] is true when [f] maps the domain [(0..n-1)] into [(0..m-1)] *) (** `range f n m` is true when `f` maps the domain `(0..n-1)` into `(0..m-1)` *) predicate injective (f: int -> int) (n: int) (m:int) = forall i j: int. 0 <= i < j < n -> f i <> f j (** [injective f n m] is true when [f] is an injection from [(0..n-1)] to [(0..m-1)] *) (** `injective f n m` is true when `f` is an injection from `(0..n-1)` to `(0..m-1)` *) ... ... @@ -148,9 +148,9 @@ module PatienceCode | Cons s rem -> wf_rev_append_stacks rem (Cons s s2) end (** [push_card c stacks acc] pushes card [c] on stacks [stacks], assuming [acc] is an accumulator (in reverse order) of stacks where [c] could not be pushed. (** `push_card c stacks acc` pushes card `c` on stacks `stacks`, assuming `acc` is an accumulator (in reverse order) of stacks where `c` could not be pushed. *) let rec push_card (c:card) (stacks : list (list card)) (acc : list (list card)) : list (list card) ... ... @@ -161,11 +161,11 @@ module PatienceCode = match stacks with | Nil -> (* we put card [c] in a new stack *) (* we put card `c` in a new stack *) rev_append (Cons (Cons c Nil) acc) Nil | Cons stack remaining_stacks -> match stack with | Nil -> absurd (* because [wf_stacks stacks] *) | Nil -> absurd (* because `wf_stacks stacks` *) | Cons c' _ -> if c <= c' then (* card is placed on the leftmost stack where its card ... ... @@ -196,7 +196,7 @@ module PatienceCode play_cards input Nil (** test, can be run using [why3 patience.mlw --exec PatienceCode.test] *) (** test, can be run using `why3 patience.mlw --exec PatienceCode.test` *) let test () = (** the list given in the problem description 9, 7, 10, 9, 5, 4, and 10 *) ... ... @@ -238,18 +238,18 @@ module PatienceAbstract (** number of cards already seen *) ghost mutable values : map int card; (** cards values seen, indexed in the order they have been seen, from  to [num_elts-1] *) from `0` to `num_elts-1` *) ghost mutable stack_sizes : map int int; (** sizes of these stacks, numbered from  to [num_stacks - 1] *) (** sizes of these stacks, numbered from `0` to `num_stacks - 1` *) ghost mutable stacks : map int (map int int); (** indexes of the cards in respective stacks *) ghost mutable positions : map int (int,int); (** table that given a card index, provides its position, i.e. in which stack it is and at which height *) ghost mutable preds : map int int; (** predecessors of cards, i.e. for each card index [i], [preds[i]] (** predecessors of cards, i.e. for each card index `i`, `preds[i]` provides an index of a card in the stack on the immediate left, whose value is smaller. Defaults to [-1] if the card is on the whose value is smaller. Defaults to `-1` if the card is on the leftmost stack. *) } ... ... @@ -273,8 +273,8 @@ module PatienceAbstract 0 <= ip < s.stack_sizes[is] && st[ip] = i) (** the position table of cards is correct, i.e. when [(is,ip) = s.positions[i]] then card [i] indeed occurs in stack [is] at height [ip] *) `(is,ip) = s.positions[i]` then card `i` indeed occurs in stack `is` at height `ip` *) /\ (forall is. 0 <= is < s.num_stacks -> forall ip. 0 <= ip < s.stack_sizes[is] -> let idx = s.stacks[is][ip] in ... ... @@ -293,15 +293,15 @@ module PatienceAbstract /\ (forall i. 0 <= i < s.num_elts -> let pred = s.preds[i] in -1 <= pred < s.num_elts && (** the predecessor is a valid index or [-1] *) (** the predecessor is a valid index or `-1` *) pred < i /\ (** predecessor is always a smaller index *) let is,_ip = s.positions[i] in if pred < 0 then is = 0 (** if predecessor is [-1] then [i] is in leftmost stack *) (** if predecessor is `-1` then `i` is in leftmost stack *) else s.values[pred] < s.values[i] /\ (** if predecessor is not [-1], it denotes a card with smaller value... *) (** if predecessor is not `-1`, it denotes a card with smaller value... *) is > 0 && (** ...the card is not on the leftmost stack... *) let ps,_pp = s.positions[pred] in ... ... @@ -315,7 +315,7 @@ module PatienceAbstract use import ref.Ref exception Return int (** [play_card c i s] pushes the card [c] on state [s] *) (** `play_card c i s` pushes the card `c` on state `s` *) let ghost play_card (c:card) (s:state) : unit requires { inv s } writes { s } ... ... @@ -571,7 +571,7 @@ module PatienceFull exception Return (** FIXME: not proved (*** FIXME: not proved let play_card (c:card) (old_stacks : list (list card)) (ghost state:state) : list (list card) requires { inv state } ... ... @@ -676,7 +676,7 @@ module PatienceFull *) (*i a version closer to the original code (*** a version closer to the original code let play_card (c:card) (old_stacks : list (list card)) (ghost state:state) : list (list card) requires { inv state } requires { glue state old_stacks } ... ... @@ -721,11 +721,11 @@ module PatienceFull *) (** {3 playing cards} *) (*** {3 playing cards} *) (* (*** let rec play_cards (input: list card) (stacks: list (list card)) ... ... @@ -756,9 +756,9 @@ module PatienceFull (** {3 playing a whole game} *) (*** {3 playing a whole game} *) (* (*** type seq 'a = { seqlen: int; seqval: map int 'a } (** a sequence is defined by a length and a mapping *) ... ...
 ... ... @@ -46,13 +46,13 @@ theory Solution type solution = map int int (** solutions [t] and [u] have the same prefix [\[0..i\[] *) (** solutions `t` and `u` have the same prefix `[0..i[` *) predicate eq_prefix (t u: map int 'a) (i: int) = forall k: int. 0 <= k < i -> t[k] = u[k] predicate eq_sol (t u: solution) = eq_prefix t u n (** [s] stores a partial solution, for the rows [0..k-1] *) (** `s` stores a partial solution, for the rows `0..k-1` *) predicate partial_solution (k: int) (s: solution) = forall i: int. 0 <= i < k -> 0 <= s[i] < n /\ ... ... @@ -71,7 +71,7 @@ theory Solution type solutions = map int solution (** [s\[a..b\[] is sorted for [lt_sol] *) (** `s[a..b[` is sorted for `lt_sol` *) predicate sorted (s: solutions) (a b: int) = forall i j: int. a <= i < j < b -> lt_sol s[i] s[j] ... ... @@ -242,7 +242,7 @@ module NQueensBits use import int.Int val ghost col: ref solution (* solution under construction *) (* val ghost k : ref int (\* current row in the current solution *\) *) (* val ghost k : ref int (* current row in the current solution *) *) val ghost sol: ref solutions (* all solutions *) val ghost s : ref int (* next slot for a solution = ... ...
 ... ... @@ -175,8 +175,8 @@ module InfinityOfRegisters use import Spec use import DWP (** [compile e r] returns a list of instructions that stores the value of [e] in register [r], without modifying any register [r' < r]. *) (** `compile e r` returns a list of instructions that stores the value of `e` in register `r`, without modifying any register `r' < r`. *) let rec compile (e: expr) (r: register) : hcode variant { e } ... ... @@ -215,8 +215,8 @@ module FiniteNumberOfRegisters val constant k: int ensures { 2 <= result } (** [compile e r] returns a list of instructions that stores the value of [e] in register [r], without modifying any register [r' < r]. *) (** `compile e r` returns a list of instructions that stores the value of `e` in register `r`, without modifying any register `r' < r`. *) let rec compile (e: expr) (r: register) : hcode requires { 0 <= r < k } ... ... @@ -249,7 +249,7 @@ module OptimalNumberOfRegisters use import Spec use import DWP (** we have k registers, namely 0,1,...,k-1, (** we have `k` registers, namely `0,1,...,k-1`, and there are at least two of them, otherwise we can't add *) val constant k: int ensures { 2 <= result } ... ... @@ -264,10 +264,10 @@ module OptimalNumberOfRegisters if n1 = n2 then 1 + n1 else max n1 n2 end (** Note: This is of course inefficient to recompute function [n] many times. A realistic implementation would compute [n e] once for each sub-expression [e], either with a first pass of tree decoration, or with function [compile] returning the value of [n e] as well, (** Note: This is of course inefficient to recompute function `n` many times. A realistic implementation would compute `n e` once for each sub-expression `e`, either with a first pass of tree decoration, or with function `compile` returning the value of `n e` as well, in a bottom-up way *) function measure (e: expr) : int = ... ... @@ -280,8 +280,8 @@ module OptimalNumberOfRegisters lemma measure_nonneg: forall e. measure e >= 0 (** [compile e r] returns a list of instructions that stores the value of [e] in register [r], without modifying any register [r' < r]. *) (** `compile e r` returns a list of instructions that stores the value of `e` in register `r`, without modifying any register `r' < r`. *) let rec compile (e: expr) (r: register) : hcode requires { 0 <= r < k } ... ...
 ... ... @@ -2,9 +2,9 @@ (** {1 Removing duplicate elements in an array} Given an array [a] of size [n], removes its duplicate elements, in-place, as follows: return [r] such that [a[0..r-1]] contains the same elements as [a[0..n-1]] and no duplicate Given an array `a` of size `n`, removes its duplicate elements, in-place, as follows: return `r` such that `a[0..r-1]` contains the same elements as `a[0..n-1]` and no duplicate *) ... ... @@ -16,11 +16,11 @@ module Spec use export int.Int use export array.Array (** v appears in [a[0..s-1]] *) (** `v` appears in `a[0..s-1]` *) predicate appears (v: 'a) (a: array 'a) (s: int) = exists i: int. 0 <= i < s /\ a[i] = v (** [a[0..s-1]] contains no duplicate element *) (** `a[0..s-1]` contains no duplicate element *) predicate nodup (a: array 'a) (s: int) = forall i: int. 0 <= i < s -> not (appears a[i] a i) ... ...
 ... ... @@ -2,8 +2,8 @@ (** {1 Removing duplicate elements in an array, using a mutable set} Given an array [a] of size [n], returns a fresh array containing the elements of [a] without duplicates, using a mutable set Given an array `a` of size `n`, returns a fresh array containing the elements of `a` without duplicates, using a mutable set (typically a hash table). *) ... ... @@ -15,11 +15,11 @@ module Spec use export int.Int use export array.Array (** v appears in [a[0..s-1]] *) (** `v` appears in `a[0..s-1]` *) predicate appears (v: 'a) (a: array 'a) (s: int) = exists i: int. 0 <= i < s /\ a[i] = v (** [a[0..s-1]] contains no duplicate element *) (** `a[0..s-1]` contains no duplicate element *) predicate nodup (a: array 'a) (s: int) = forall i: int. 0 <= i < s -> not (appears a[i] a i) ... ...
 ... ... @@ -34,7 +34,7 @@ module Residuals forall c w r. mem (Cons c w) (Star r) -> exists w1 w2. w = w1 ++ w2 /\ mem (Cons c w1) r /\ mem w2 (Star r) (** [residual r c] denotes the set of words [w] such that [mem c.w r] *) (** `residual r c` denotes the set of words `w` such that `mem c.w r` *) let rec residual (r:regexp) (c:char) : regexp variant { r } ensures { forall w. mem w result <-> mem (Cons c w) r } ... ...
 ... ... @@ -249,7 +249,7 @@ module Balance ensures { 2 <= result } function string_of_array (q: Array.array rope) (l u: int) : string (** [q[u-1] + q[u-2] + ... + q[l]] *) (** `q[u-1] + q[u-2] + ... + q[l]` *) axiom string_of_array_empty: forall q: Array.array rope, l: int. ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!