Commit 1b197bd7 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Convert some more examples.

parent d1d252b9
......@@ -135,7 +135,7 @@ predicate eval_fmla (sigma:env) (pi:stack) (f:fmla) =
end
(** [valid_fmla f] is true when [f] is valid in any environment *)
(** `valid_fmla f` is true when `f` is valid in any environment *)
predicate valid_fmla (p:fmla) = forall sigma:env, pi:stack. eval_fmla sigma pi p
......@@ -415,8 +415,8 @@ lemma Cons_append: forall a: 'a, l1 l2: list 'a.
lemma Append_nil_l:
forall l: list 'a. Nil ++ l = l
(** substitution of a reference [x] by a logic variable [v]
warning: proper behavior only guaranted if [v] is fresh *)
(** substitution of a reference `x` by a logic variable `v`
warning: proper behavior only guaranted if `v` is fresh *)
function msubst_term (t:term) (x:mident) (v:ident) : term =
match t with
......@@ -437,7 +437,7 @@ function msubst (f:fmla) (x:mident) (v:ident) : fmla =
end
(** [fresh_in_term id t] is true when [id] does not occur in [t] *)
(** `fresh_in_term id t` is true when `id` does not occur in `t` *)
predicate fresh_in_term (id:ident) (t:term) =
match t with
| Tvalue _ | Tderef _ -> true
......
......@@ -77,8 +77,8 @@ predicate eval_fmla (sigma:env) (pi:env) (f:fmla) =
eval_fmla sigma (IdMap.set pi x (Vbool b)) f
end
(** substitution of a reference [r] by a logic variable [v]
warning: proper behavior only guaranted if [v] is fresh *)
(** substitution of a reference `r` by a logic variable `v`
warning: proper behavior only guaranted if `v` is fresh *)
let rec function subst_term (e:term) (r:ident) (v:ident) : term =
match e with
......
......@@ -8,15 +8,15 @@ theory SelectionTypes
use import seq.Seq
use import option.Option
(** Describe a position in the sequence [left ++ middle ++ right]
(see [rebuild]) *)
(** Describe a position in the sequence `left ++ middle ++ right`
(see `rebuild`) *)
type split 'a = {
left : seq 'a;
middle : option 'a;
right : seq 'a;
}
(** Describe reduced problem for selection (see [selected_part]) *)
(** Describe reduced problem for selection (see `selected_part`) *)
type part_base 'a = Left 'a
| Right 'a
| Here
......@@ -66,9 +66,9 @@ module AVL
(** The implementation is parameterized by an abstract monoid.
The elements of the monoid will be used as summaries of
sequence of elements, obtained by aggregation of the elements of
the sequence. In other words, [M.sum f [a_1;...;a_n]] is the
monoidal summary of sequence [[a_1;...;a_n]] with respect to
measure [f]. *)
the sequence. In other words, `M.sum f [a_1;...;a_n]` is the
monoidal summary of sequence `[a_1;...;a_n]` with respect to
measure `f`. *)
clone monoid.ComputableMonoid as M
clone monoid.MonoidSum as M with
(* scope M = M *)
......@@ -148,7 +148,7 @@ module AVL
2) The monoidal value corresponds to the summary of the sequence of
elements associated with the subtree associated with the node
3) Left and right subtrees are [balancing]-height-balanced *)
3) Left and right subtrees are `balancing`-height-balanced *)
predicate balanced (t:tree 'a) = match t with
| Empty -> true
| Node l _ r h m -> h = real_height t /\
......@@ -258,12 +258,12 @@ module AVL
s
end
(** First re-balancing constructor: [balance l d r]
build the same sequence as [node l d r], but permit slightly
(** First re-balancing constructor: `balance l d r`
build the same sequence as `node l d r`, but permit slightly
unbalanced input, and might decrement the expected height by one.
Also, if the expected input node was already balanced, it is
specified to return a value indistinguishable from a value
returned by [node l d r].
returned by `node l d r`.
This constructor is constant-time. *)
let balance (l:t 'a) (d:D.t 'a) (r:t 'a) : t 'a
requires { -balancing-1 <= l.hgt - r.hgt <= balancing+1 }
......@@ -303,7 +303,7 @@ module AVL
end
else node l d r
(** Internal routine. Decompose [l ++ [d] ++ r] as [[head]++tail],
(** Internal routine. Decompose `l ++ [d] ++ r` as `[head]++tail`,
with sequences represented by AVL trees. *)
let rec decompose_front_node (l:t 'a) (d:D.t 'a) (r:t 'a) : (D.t 'a,t 'a)
requires { -balancing <= l.hgt - r.hgt <= balancing }
......@@ -328,7 +328,7 @@ module AVL
end
(** Internal routine, mirror of [decompose_front_node]. *)
(** Internal routine, mirror of `decompose_front_node`. *)
let rec decompose_back_node (l:t 'a) (d:D.t 'a) (r:t 'a) : (t 'a,D.t 'a)
requires { -balancing <= l.hgt - r.hgt <= balancing }
returns { (res:t 'a,d2) -> node_model l d r = snoc res d2 /\
......@@ -404,7 +404,7 @@ module AVL
end
end
(** List cons: build the sequence [cons d t]. logarithmic-time. *)
(** List cons: build the sequence `cons d t`. logarithmic-time. *)
let rec cons (d:D.t 'a) (t:t 'a) : t 'a
ensures { result = cons d t }
ensures { 1 >= result.hgt - t.hgt >= 0 }
......@@ -414,7 +414,7 @@ module AVL
| ANode l d2 r _ _ -> balance (cons d l) d2 r
end
(** Reverse cons: build [snoc t d]. logarithmic-time. *)
(** Reverse cons: build `snoc t d`. logarithmic-time. *)
let rec snoc (t:t 'a) (d:D.t 'a) : t 'a
ensures { result = snoc t d }
ensures { 1 >= result.hgt - t.hgt >= 0 }
......@@ -426,7 +426,7 @@ module AVL
(** Variant of the node constructor without any height hypothesis.
The time complexity is proportional to the height
difference between [l] and [r] (O(|l.m.hgt-r.m.hgt|)) (in particular,
difference between `l` and `r` (O(|l.m.hgt-r.m.hgt|)) (in particular,
it is logarithmic) *)
let rec join (l:t 'a) (d:D.t 'a) (r:t 'a) : t 'a
ensures { result = node_model l d r }
......@@ -488,7 +488,7 @@ module AVL
random access.
The positions found in step 1) corresponds readily to splits of
the sequence, as defined in the [SelectionTypes] module. We consider
the sequence, as defined in the `SelectionTypes` module. We consider
that the objective of the search is to find a split with particular
properties.
......@@ -523,7 +523,7 @@ module AVL
3) Taking the split induced by the node *)
type part = part_base selector
(** Parameter: [selected_part llis rlis s l d r] effectively compute
(** Parameter: `selected_part llis rlis s l d r` effectively compute
the reduction of the selection to one of the three part of a node.
It uses the monoidal summaries to get informations about the
left and right subtrees. *)
......@@ -551,10 +551,10 @@ module AVL
ref { left = S.empty; middle = None; right = S.empty }
(** Insertion of an element into the sequence.
[insert r s d t] split the sequence [t] using [s] as [lf ++ o ++ rg],
and rebuild it with [d] in the middle, potentially erasing whatever
was there before, as [lf ++ [d] ++ rg].
The reference [r] is assigned to the selected position.
`insert r s d t` split the sequence `t` using `s` as `lf ++ o ++ rg`,
and rebuild it with `d` in the middle, potentially erasing whatever
was there before, as `lf ++ [d] ++ rg`.
The reference `r` is assigned to the selected position.
It is logarithmic-time.
Note: the procedure described above match only the specification,
not what the actual code does. *)
......@@ -583,9 +583,9 @@ module AVL
end
(** Remove an element from the sequence.
[remove r s t] Split the sequence [t] using [s] into [lf ++ o ++ rg],
`remove r s t` Split the sequence `t` using `s` into `lf ++ o ++ rg`,
and erase whatever may be in the middle,
as [lf++rg]. logarithmic-time. *)
as `lf++rg`. logarithmic-time. *)
let rec remove (ghost r:ref (split (D.t 'a))) (s:selector) (t:t 'a) : t 'a
requires { selection_possible s t }
ensures { result = !r.left ++ !r.right }
......@@ -609,8 +609,8 @@ module AVL
end
(** Attempt to find an element in the sequence.
[find r s t] return the middle value obtained by splitting the
sequence [t] with respect to the [s]. logarithmic-time. *)
`find r s t` return the middle value obtained by splitting the
sequence `t` with respect to the `s`. logarithmic-time. *)
let rec get (ghost r:ref (split (D.t 'a))) (s:selector)
(t:t 'a) : option (D.t 'a)
requires { selection_possible s t }
......@@ -634,7 +634,7 @@ module AVL
end
end
(** Combine [get] and [remove] *)
(** Combine `get` and `remove` *)
let rec extract (ghost r:ref (split (D.t 'a))) (s:selector)
(t:t 'a) : (option (D.t 'a),t 'a)
requires { selection_possible s t }
......@@ -663,8 +663,8 @@ module AVL
end
(** Split a sequence.
[split r s t] return a program version of a split found
by [s], using AVL trees for the sequence. It is logarithmic-time.
`split r s t` return a program version of a split found
by `s`, using AVL trees for the sequence. It is logarithmic-time.
Note: As their specification suggest, all the binary-search-based
routines can be directly implemented in term of a split followed
by catenations. Although a constant time factor, the rebalancing work
......
......@@ -61,7 +61,7 @@ module RAL
predicate selection_possible (s:selector) (l:seq 'a) =
0 <= s.index && (if s.hole then s.index <= length l else s.index < length l)
(** Selection predicate: We are exactly at the [index]-th position of the
(** Selection predicate: We are exactly at the `index`-th position of the
rebuild sequence, and there is an element in the middle iff we are
not trying to select a hole. *)
predicate selected (s:selector) (e:split 'a) =
......@@ -276,4 +276,3 @@ module RAL
check { a[1] = 2 }
end
......@@ -384,7 +384,7 @@ module MapBase
assert { selected d.key s };
{ field = Sel.join l.field d r.field }
(** Add every element from [a] into [t]. *)
(** Add every element from `a` into `t`. *)
let rec add_all (a:t 'a) (t:t 'a) : t 'a
ensures { forall k. result.domn k <-> a.domn k \/ t.domn k }
ensures { forall k. a.domn k -> result.func k = a.func k }
......@@ -412,8 +412,8 @@ module MapBase
end
end
(** Create the table with the elements of [a]
whose key appear in [p]. *)
(** Create the table with the elements of `a`
whose key appear in `p`. *)
let rec filter (p:t 'b) (a:t 'a) : t 'a
ensures { forall k. result.domn k <-> a.domn k /\ p.domn k }
ensures { forall k. result.domn k -> result.func k = a.func k }
......@@ -441,8 +441,8 @@ module MapBase
end
end
(** Complement of [filter]: remove from [a] every element whose
key appear in [p]. *)
(** Complement of `filter`: remove from `a` every element whose
key appear in `p`. *)
let rec remove_all (p:t 'b) (a:t 'a) : t 'a
ensures { forall k. result.domn k <-> a.domn k /\ not p.domn k }
ensures { forall k. result.domn k -> result.func k = a.func k }
......@@ -468,7 +468,7 @@ module MapBase
end
(** Create a table with the elements that appear
exactly in one of [a] and [b], but not both. *)
exactly in one of `a` and `b`, but not both. *)
let rec symdiff (a b:t 'a) : t 'a
ensures { forall k. result.domn k <-> not (a.domn k <-> b.domn k) }
ensures { forall k. result.domn k /\ a.domn k -> result.func k = a.func k }
......@@ -652,7 +652,7 @@ module Map
| Some (_,v) -> Some v
end
(** Set the binding for key [k], erasing any such previous binding. *)
(** Set the binding for key `k`, erasing any such previous binding. *)
let insert (k0:K.t) (v:'a) (t:t 'a) : t 'a
ensures { result.card = if t.domn k0 then t.card else t.card + 1 }
ensures { forall k. CO.eq k k0 -> result.domn k /\ result.func k = v }
......@@ -662,7 +662,7 @@ module Map
result.func k = t.func k }
= MB.insert (k0,v) t
(** Erase any potential binding for key [k]. *)
(** Erase any potential binding for key `k`. *)
let remove (k0:K.t) (t:t 'a) : t 'a
ensures { result.card = if t.domn k0 then t.card - 1 else t.card }
ensures { forall k. CO.eq k k0 -> not result.domn k }
......@@ -673,8 +673,8 @@ module Map
= MB.remove k0 t
(** Split the table in three parts:
Bindings with key lower than [k], value associated to [k],
and bindings with key greater than [k]. *)
Bindings with key lower than `k`, value associated to `k`,
and bindings with key greater than `k`. *)
let split (k0:K.t) (t:t 'a) : (t 'a,option 'a,t 'a)
returns { (lf:t 'a,o,rg:t 'a) ->
(forall k. CO.lt k k0 -> lf.domn k <-> t.domn k) /\
......@@ -849,9 +849,9 @@ module Set
ensures { forall k. not CO.eq k k0 -> result.set k <-> t.set k }
= MB.remove k0 t
(** Split the set into three parts: elements lower than [k],
elements equal to [k],
and elements bigger than [k] *)
(** Split the set into three parts: elements lower than `k`,
elements equal to `k`,
and elements bigger than `k` *)
let split (k0:K.t) (t:t) : (t,bool,t)
returns { (lf:t,b,rg:t) ->
(forall k. CO.lt k k0 -> lf.set k <-> t.set k) /\
......
......@@ -48,7 +48,7 @@ module Puzzle8
use import Roberval
use import array.Array
(** All values in [balls(lo..hi-1)] are equal to [w], apart from [balls[lb]]
(** All values in `balls[lo..hi-1]` are equal to `w`, apart from `balls[lb]`
which is smaller. *)
predicate spec (balls: array int) (lo hi: int) (lb w: int) =
0 <= lo <= lb < hi <= length balls &&
......@@ -56,7 +56,7 @@ module Puzzle8
balls[lb] < w
(** Solve the problem for 3 balls, using exactly one weighing.
The solution [lb] is passed as a ghost argument. *)
The solution `lb` is passed as a ghost argument. *)
let solve3 (balls: array int) (lo: int) (ghost lb: int) (ghost w: int) : int
requires { !counter >= 1 }
requires { spec balls lo (lo + 3) lb w }
......@@ -70,7 +70,7 @@ module Puzzle8
end
(** Solve the problem for 8 balls, using exactly two weighings.
The solution [lb] is passed as a ghost argument. *)
The solution `lb` is passed as a ghost argument. *)
let solve8 (balls: array int) (ghost lb: int) (ghost w: int) : int
requires { !counter = 2 }
requires { spec balls 0 8 lb w }
......@@ -100,8 +100,8 @@ module Puzzle12
use import Roberval
use import array.Array
(** The index [j] of the intruder, its status [b] (whether it is
lighter or heavier), and the weight [w] of the other balls are
(** The index `j` of the intruder, its status `b` (whether it is
lighter or heavier), and the weight `w` of the other balls are
all passed as ghost arguments. *)
let solve12 (balls: array int) (ghost w j: int) (ghost b: bool) : (int, bool)
requires { !counter = 3 }
......
......@@ -25,7 +25,7 @@ module BinomialHeap
(** Trees.
These are arbitrary trees, not yet constrained
to be binomial trees. Field [rank] is used later to store the rank
to be binomial trees. Field `rank` is used later to store the rank
of the binomial tree, for access in constant time. *)
type tree = {
......@@ -50,7 +50,7 @@ module BinomialHeap
(** Heaps. *)
(* [e] is no greater than the roots of the trees in [l] *)
(* `e` is no greater than the roots of the trees in `l` *)
predicate le_roots (e: elt) (l: list tree) =
match l with
| Nil -> true
......@@ -106,7 +106,7 @@ module BinomialHeap
| Cons { children = c } r -> heaps_mem c; heaps_mem r
end
(** Binomial tree of rank [k]. *)
(** Binomial tree of rank `k`. *)
predicate has_order (k: int) (l: list tree) =
match l with
......@@ -127,8 +127,8 @@ module BinomialHeap
type heap = list tree
(** A heap [h] is a list of binomial trees in strict increasing order of
ranks, those ranks being no smaller than [m]. *)
(** A heap `h` is a list of binomial trees in strict increasing order of
ranks, those ranks being no smaller than `m`. *)
predicate inv (m: int) (h: heap) =
match h with
......
......@@ -358,7 +358,7 @@ module AsciiCode
assert { numof (fun_or (nth b) (nth c)) 0 32 = numof (nth b) 0 32 + numof (nth c) 0 32 };
assert { numof (nth (bw_or b c)) 0 32 = numof (fun_or (nth b) (nth c)) 0 32 }
(** The [ascii] function makes any character valid in the
(** The `ascii` function makes any character valid in the
sense that we just defined. One way to implement it is to count
the number of 1-bits of a character encoded on 7 bits, and if this
number is odd, set the 8th bit to 1 if not, do nothing. *)
......
......@@ -40,7 +40,7 @@ module Bitwalker
assert { BV64.eq_sub_bv x BV64.zeros (C32_64.toBig len) (BV64.sub (BV64.of_int 64) (C32_64.toBig len))
<-> BV64.ult x (maxvalue len) }
(** return [value] with the bit of index [left] from the left set to [flag] *)
(** return `value` with the bit of index `left` from the left set to `flag` *)
let poke_64bit_bv (value : BV64.t) (left : BV32.t) (flag : bool) : BV64.t
requires { BV32.t'int left < 64 }
ensures { forall i. 0 <= i < 64 /\ i <> 63 - BV32.t'int left ->
......@@ -64,8 +64,8 @@ module Bitwalker
end
end
(** return [value] with the bit of index [left] from the left set to [flag] *)
(* version where [left] is an int and not a bitvector, which
(** return `value` with the bit of index `left` from the left set to `flag` *)
(* version where `left` is an int and not a bitvector, which
is closer to the result of the SPARK translation from signed
integers *)
let poke_64bit (value : BV64.t) (left : int) (flag : bool) : BV64.t
......@@ -92,7 +92,7 @@ module Bitwalker
end
(* return the bit of [byte] at position [left] starting from the
(* return the bit of `byte` at position `left` starting from the
left *)
let peek_8bit_bv (byte : BV8.t) (left : BV32.t) : bool
......@@ -110,7 +110,7 @@ module Bitwalker
not (BV32.eq (BV32.bw_and (C8_32.toBig byte) mask) BV32.zeros)
end
(* return the bit of the [left]/8 element of [addr] at position mod [left] 8 starting from the left *)
(* return the bit of the `left`/8 element of `addr` at position mod `left` 8 starting from the left *)
let peek_8bit_array (addr : array BV8.t) (left : BV32.t) : bool
requires { 8 * (length addr) < BV32.two_power_size }
requires { BV32.t'int left < 8 * length addr }
......@@ -118,8 +118,8 @@ module Bitwalker
=
peek_8bit_bv (addr[ BV32.to_uint (BV32.udiv_check left (8:BV32.t)) ]) (BV32.urem_check left (8:BV32.t))
(* return a bitvector of 64 bits with its [len] bits of the right
set to the bits between [start] and [start] + [len] of [addr] *)
(* return a bitvector of 64 bits with its `len` bits of the right
set to the bits between `start` and `start+len` of `addr` *)
let peek (start : BV32.t) (len : BV32.t) (addr : array BV8.t) : BV64.t
requires { BV32.t'int len <= 64 }
requires { BV32.t'int start + BV32.t'int len < BV32.two_power_size }
......@@ -185,7 +185,7 @@ module Bitwalker
}
*)
(* return [byte] with the bit at index [left] from the left set to [flag] *)
(* return `byte` with the bit at index `left` from the left set to `flag` *)
let poke_8bit (byte : BV8.t) (left : BV32.t) (flag : bool) : BV8.t
requires { BV32.t'int left < 8 }
ensures { forall i:int. 0 <= i < 8 -> i <> 7 - BV32.t'int left ->
......
......@@ -6,26 +6,26 @@ module M
use import ref.Ref
(* Parameters.
Without loss of generality, we can take [x1=0] and [y1=0].
Thus the line to draw joins [(0,0)] to [(x2,y2)]
and we have [deltax = x2] and [deltay = y2].
Without loss of generality, we can take `x1=0` and `y1=0`.
Thus the line to draw joins `(0,0)` to `(x2,y2)`
and we have `deltax = x2` and `deltay = y2`.
Moreover we assume being in the first octant, i.e.
[0 <= y2 <= x2]. The seven other cases can be easily
`0 <= y2 <= x2`. The seven other cases can be easily
deduced by symmetry. *)
(* [best x y] expresses that the point [(x,y)] is the best
(* `best x y` expresses that the point `(x,y)` is the best
possible point i.e. the closest to the real line
i.e. for all y', we have |y - x*y2/x2| <= |y' - x*y2/x2|
We stay in type [int] by multiplying everything by [x2]. *)
i.e. for all `y'`, we have `|y - x*y2/x2| <= |y' - x*y2/x2|`
We stay in type `int` by multiplying everything by `x2`. *)
use import int.Abs
predicate best (x2 y2 x y: int) =
forall y': int. abs (x2 * y - x * y2) <= abs (x2 * y' - x * y2)
(** Key lemma for Bresenham's proof: if [b] is at distance less or equal
than [1/2] from the rational [c/a], then it is the closest such integer.
We express this property using integers by multiplying everything by [2a]. *)
(** Key lemma for Bresenham's proof: if `b` is at distance less or equal
than `1/2` from the rational `c/a`, then it is the closest such integer.
We express this property using integers by multiplying everything by `2a`. *)
lemma closest :
forall a b c: int.
......
......@@ -137,7 +137,7 @@ use import Expr
(** {4 Exercise 0.1}
CPS-transform (call by value, left to right) the function [eval_0],
CPS-transform (call by value, left to right) the function `eval_0`,
and call it from the main interpreter with the identity function as
initial continuation
{h <blockquote><pre>
......@@ -175,7 +175,7 @@ use import DirectSem
(** {4 Exercise 0.2}
De-functionalize the continuation of [eval_1].
De-functionalize the continuation of `eval_1`.
{h <blockquote><pre>
cont ::= ...
......@@ -183,9 +183,9 @@ use import DirectSem
eval_2 : expression -> cont -> value
interpret_2 : program -> value
</pre></blockquote>}
The data type [cont] represents the grammar of contexts.
The data type `cont` represents the grammar of contexts.
The two mutually recursive functions [eval_2] and [continue_2]
The two mutually recursive functions `eval_2` and `continue_2`
implement an abstract machine, that is a state transition system.
*)
......@@ -239,7 +239,7 @@ function size_c (c:cont) : int =
lemma size_c_pos: forall c: cont. size_c c >= 0
(** WhyML programs (declared with [let] instead of [function]),
(** WhyML programs (declared with `let` instead of `function`),
mutually recursive, resulting from de-functionalization *)
let rec continue_2 (c:cont) (v:int) : int
......@@ -262,7 +262,7 @@ with eval_2 (e:expr) (c:cont) : int
end
(** The interpreter. The post-condition specifies that this program
computes the same thing as [eval_0] *)
computes the same thing as `eval_0` *)
let interpret_2 (p:prog) : int
ensures { result = eval_0 p }
......@@ -287,7 +287,7 @@ use import DirectSem
(** {4 Exercise 0.2}
De-functionalize the continuation of [eval_1].
De-functionalize the continuation of `eval_1`.
{h <blockquote><pre>
cont ::= ...
......@@ -295,9 +295,9 @@ use import DirectSem
eval_2 : expression -> cont -> value
interpret_2 : program -> value
</pre></blockquote>}
The data type [cont] represents the grammar of contexts.
The data type `cont` represents the grammar of contexts.
The two mutually recursive functions [eval_2] and [continue_2]
The two mutually recursive functions `eval_2` and `continue_2`
implement an abstract machine, that is a state transition system.
*)
......@@ -349,7 +349,7 @@ function size_c (c:cont) (acc:nat) : nat =
| A2 _ k -> S (size_c k acc)
end
(** WhyML programs (declared with [let] instead of [function]),
(** WhyML programs (declared with `let` instead of `function`),
mutually recursive, resulting from de-functionalization *)
let rec continue_2 (c:cont) (v:int) : int
......@@ -372,7 +372,7 @@ with eval_2 (e:expr) (c:cont) : int
end
(** The interpreter. The post-condition specifies that this program
computes the same thing as [eval_0] *)
computes the same thing as `eval_0` *)
let interpret_2 (p:prog) : int
ensures { result = eval_0 p }
......@@ -429,11 +429,11 @@ e1 => n1 e2 => n2 n1 >= n2 n1 - n2 = n3
---------------------------------------------
e1 - e2 => n3
</pre></blockquote>}
We interpret the program [e] into value [n] if the judgement
We interpret the program `e` into value `n` if the judgement
{h <blockquote><pre>
e => n
</pre></blockquote>}
holds, and into error [s] if the judgement
holds, and into error `s` if the judgement
{h <blockquote><pre>
e => s
</pre></blockquote>}
......@@ -470,7 +470,7 @@ function interpret_0 (p:prog) : value = eval_0 p
(** {4 Exercise 1.1}
CPS-transform (call by value, from left to right)
the function [eval_0], call it from the main interpreter
the function `eval_0`, call it from the main interpreter
with the identity function as initial continuation.
{h <blockquote><pre>
eval_1 : expr -> (expressible_value -> 'a) -> 'a
......@@ -513,7 +513,7 @@ lemma cps_correct: forall p. interpret_1 p = interpret_0 p
{h <blockquote><pre>
(value -> 'a) * (error -> 'a)
</pre></blockquote>}
and adapt [eval_1] and [interpret_1] as
and adapt `eval_1` and `interpret_1` as
{h <blockquote><pre>
eval_2 : expr -> (value -> 'a) -> (error -> 'a) -> 'a
interpret_2 : program -> expressible_value
......@@ -566,7 +566,7 @@ lemma cps2_correct: forall p. interpret_2 p = interpret_0 p
(** {4 Exercise 1.3}
Specialize the codomain of the continuations and of the evaluation function
so that it is not polymorphic anymore but is [expressible_value], and
so that it is not polymorphic anymore but is `expressible_value`, and
then short-circuit the second continuation to stop in case of error
{h <blockquote><pre>
eval_3 : expr -> (value -> expressible_value) -> expressible_value
......@@ -610,7 +610,7 @@ lemma cps3_correct: forall p. interpret_3 p = interpret_0 p
(** {4 Exercise 1.4}
De-functionalize the continuation of [eval_3].
De-functionalize the continuation of `eval_3`.
{h <blockquote><pre>
cont ::= ...
......@@ -618,10 +618,10 @@ lemma cps3_correct: forall p. interpret_3 p = interpret_0 p
eval_4 : expr -> cont -> expressible_value
interprete_4 : program -> expressible_value
</pre></blockquote>}
The data type [cont] represents the grammar of contexts.
The data type `cont` represents the grammar of contexts.
(NB. has it changed w.r.t to previous exercise?)
The two mutually recursive functions [eval_4] and [continue_4]
The two mutually recursive functions `eval_4` and `continue_4`
implement an abstract machine, that is a transition system that
stops immediately in case of error, or and the end of computation.
......@@ -707,7 +707,7 @@ with eval_4 (e:expr) (c:cont) : value
end
(** The interpreter. The post-condition specifies that this program
computes the same thing as [eval_0] *)
computes the same thing as `eval_0` *)
let interpret_4 (p:prog) : value
ensures { result = eval_0 p }
......@@ -995,7 +995,7 @@ let rec itere (e:expr) : int
(** {4 Exercise 2.1}
Optimize the step recomposition / decomposition
into a single function [refocus].
into a single function `refocus`.
*)
......
......@@ -3,11 +3,11 @@
The Art of Computer Programming, vol 1, page 147.
The following code computes a table of the first [m] prime numbers.
The following code computes a table of the first `m` prime numbers.
Though there are more efficient ways of computing prime numbers,
the nice thing about this code is that it requires not less than
Bertrand's postulate (for [n > 1], there is always a prime [p] such that
[n < p < 2n]) to be proved correct.
Bertrand's postulate (for `n > 1`, there is always a prime `p` such that
`n < p < 2n`) to be proved correct.
This program had been proved correct using Coq and an early version of
Why back in 2003, by Laurent Théry (INRIA Sophia-Antipolis): Laurent Théry,
......@@ -18,9 +18,9 @@
posing Bertrand's postulate as a lemma that we do not prove.
Note: Knuth's code is entering the loop where a new prime number is
added, thus resulting into the immediate addition of 3 as [prime[1]].
It allows subsequent division tests to start at [prime[1]=3], thus
saving the division by [prime[0]=2]. We did something similar in the
added, thus resulting into the immediate addition of 3 as `prime[1]`.
It allows subsequent division tests to start at `prime[1]=3`, thus
saving the division by `prime[0]=2`. We did something similar in the
code below, though the use of a while loop looks like we did a
special case for 3 as well. *)
......@@ -37,7 +37,7 @@ module PrimeNumbers
predicate no_prime_in (l u: int) =
forall x: int. l < x < u -> not (prime x)
(** [p[0]..p[u-1]] are the first u prime numbers *)
(** `p[0]..p[u-1]` are the first u prime numbers *)
predicate first_primes (p: int -> int) (u: int) =
p[0] = 2 /\
(* sorted *)
......@@ -59,7 +59,7 @@ module PrimeNumbers
use import array.Array
(** [prime_numbers m] returns an array containing the first [m]
(** `prime_numbers m` returns an array containing the first `m`
prime numbers *)
let prime_numbers (m: int)
requires { m >= 2 }
......
......@@ -14,8 +14,8 @@ module PrimeFactor
use import number.Prime
use import number.Coprime
(** returns the smallest divisor of [n] greater than or equal to [d],
assuming no divisor between 2 and [d]. *)
(** returns the smallest divisor of `n` greater than or equal to `d`,
assuming no divisor between 2 and `d`. *)
let rec smallest_divisor (d n:int) : int
requires { 2 <= n }
requires { 2 <= d <= n }
......
......@@ -46,11 +46,11 @@ module LinearProbing
ensures { 0 <= result < n }
= mod (hash k) n
(** [j] lies between [l] and [r], cyclically *)
(** `j` lies between `l` and `r`, cyclically *)
predicate between (l j r: int) =
l <= j < r || r < l <= j || j < r < l
(** number of dummy values in array [a] between [l] and [u] *)
(** number of dummy values in array `a` between `l` and `u` *)
scope NumOfDummy
use int.NumOf
......
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