Commit 2165340a authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

terminology: code labels are renamed to (code) marks

new syntax 'L: to introduce a mark
new syntax at t 'L in logical expressions
parent a9b29015
* marks an incompatible change
o [WhyML] programs labels with new syntax 'L: (instead of label L:)
o [Coq output] fixed bug 12934: type def with several type params
o [IDE] interactive detection of provers disabled because incompatible
with session. Detection must be done with why3config --detect-provers
o WhyML with mutable record fields and type models
o [WhyML] mutable record fields and type models
o why3replayer
* "parameter" keyword renamed to "val"
* new syntax for conjunction (/\) and disjunction (\/)
......@@ -18,7 +19,7 @@
o [IDE] displays explanations using labels of the form "expl:..."
o fixed Coq output for polymorphic inductive predicates
o [IDE] dropped dependence on Sqlite
* calls to prover can now be asynchronous
* calls to prover can now be asynchronous
Driver.prove_task now returns some intermediate value (of type
prover_call), which can be queried in two ways:
- blocking way with Call_provers.wait_on_call
......@@ -41,7 +42,7 @@ version 0.64, Feb 16, 2011
* syntax: /\ renamed into && and \/ into ||
o accept lowercase names for axioms, lemmas, goals, and cases in
inductive predicates
o labels in terms and formulas are not printed by default.
o labels in terms and formulas are not printed by default.
o transformation split-goal does not split under disjunction anymore
o fixed --enable-local
o why.conf is no more looked for in the current directory; use -C or
......
......@@ -913,7 +913,7 @@ ifeq (@enable_doc@,yes)
doc: doc/manual.pdf
# doc/manual.html
BNF = qualid constant operator term type formula theory why_file \
BNF = qualid label constant operator term type formula theory why_file \
typev expr module whyml_file
BNFTEX = $(addprefix doc/, $(addsuffix _bnf.tex, $(BNF)))
......
......@@ -8,12 +8,12 @@ val x : ref int
val f : unit -> { } unit writes x { !x = 1 - old !x }
let p () =
'Init:
begin
label Init:
let t = () in ();
(f ());
(f ());
assert { !x = at !x Init };
assert { !x = at !x 'Init };
()
end
......
......@@ -12,7 +12,6 @@
| "let" "rec" recfun ("with" recfun)* ; recursive functions
| "if" expr "then" expr ("else" expr)? ; conditional
| expr ";" expr ; sequence
| "label" uident ":" expr ; label
| "loop" loop-annot "end" ; infinite loop
| "while" expr "do" loop-annot expr "done" ; while loop
| "for" lident "=" expr to-downto expr ; for loop
......@@ -32,6 +31,8 @@
| expr "." lqualid "<-" expr ; field assignment
| "{|" expr "with" field-value+ "|}" ; field update
| expr ":" type ; cast
| label expr ; label
| "'" uident ":" expr ; code mark
| "(" expr ")" ; parentheses
\
expr-case ::= pattern "->" expr ;
......
\begin{syntax}
label ::= string ;
| "#" filename digit+ digit+ digit+ "#" ;
\
filename ::= string ;%
\end{syntax}
......@@ -15,6 +15,8 @@ Comments are enclosed by \texttt{(*} and \texttt{*)} and can be nested.
\paragraph{Strings.}
Strings are enclosed in double quotes (\verb!"!). Double quotes can be
inserted in strings using the backslash character (\verb!\!).
In the following, strings are referred to with the non-terminal
\nonterm{string}{}.
% TODO: escape sequences for strings
......@@ -53,6 +55,12 @@ characters they are built from:
\item level 1: all other operators (non-terminal \textit{infix-op-1}).
\end{itemize}
\paragraph{Labels.} Identifiers, terms, formulas, program expressions
can all be labeled, either with a string, or with a location tag.
\begin{center}\framebox{\input{./label_bnf.tex}}\end{center}
A location tag consists of a file name, a line number, and starting
and ending characters.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Why3 Language}
......
......@@ -20,6 +20,7 @@
| "{|" term "with" field-value+ "|}" ; field update
| term ":" type ; cast
| label term ; label
| "'" uident ; code mark
| "(" term ")" ; parentheses
\
term-case ::= pattern "->" term ;
......
This diff is collapsed.
......@@ -612,9 +612,9 @@ The precondition relates \texttt{board}, \texttt{pos}, and \texttt{n}
and requires \texttt{board} to be a solution up to \texttt{pos}:
\begin{verbatim}
{ length board = n /\ 0 <= pos <= n /\ solution board pos }
label Init:
'Init:
\end{verbatim}
We place a label \texttt{Init} immediately after the precondition to
We place a code mark \texttt{'Init} immediately after the precondition to
be able to refer to the value of \texttt{board} in the pre-state.
Whenever we reach the end of the chess board, we have found a solution
and we signal it using exception \texttt{Solution}:
......@@ -632,7 +632,7 @@ extend this prefix with a queen on row \texttt{pos} at a column below
\texttt{i}:
\begin{verbatim}
invariant {
eq_board board (at board Init) pos /\
eq_board board (at board 'Init) pos /\
forall b:array int. length b = n -> is_board b n ->
eq_board board b pos -> 0 <= b[pos] < i -> not (solution b n) }
\end{verbatim}
......@@ -688,11 +688,11 @@ automatically, including the verification of the lemmas themselves.
let rec bt_queens (board: array int) (n: int) (pos: int) variant { n - pos } =
{ length board = n /\ 0 <= pos <= n /\ solution board pos }
label Init:
'Init:
if pos = n then raise Solution;
for i = 0 to n - 1 do
invariant {
eq_board board (at board Init) pos /\
eq_board board (at board 'Init) pos /\
forall b:array int. length b = n -> is_board b n ->
eq_board board b pos -> 0 <= b[pos] < i -> not (solution b n) }
board[pos] <- i;
......
......@@ -41,17 +41,15 @@ module Algo64
let rec quicksort (a:array int) (m:int) (n:int) : unit variant { n-m } =
{ 0 <= m <= n < length a }
label Init:
'Init:
if m < n then begin
let i = ref 0 in
let j = ref 0 in
partition a m n i j;
label L1:
quicksort a m !j;
assert { permut_sub (at a L1) a m n };
label L2:
quicksort a !i n;
assert { permut_sub (at a L2) a m n }
'L1: quicksort a m !j;
assert { permut_sub (at a 'L1) a m n };
'L2: quicksort a !i n;
assert { permut_sub (at a 'L2) a m n }
end
{ permut_sub (old a) a m n /\ sorted_sub a m n }
......
......@@ -38,12 +38,12 @@ module Algo65
if m < n then begin
let i = ref 0 in
let j = ref 0 in
label L1:
'L1:
partition a m n i j;
assert { permut_sub (at a L1) a m n };
label L2:
assert { permut_sub (at a 'L1) a m n };
'L2:
if k <= !j then find a m !j k;
assert { permut_sub (at a L2) a m n };
assert { permut_sub (at a 'L2) a m n };
if !i <= k then find a !i n k
end
{ permut_sub (old a) a m n /\
......
......@@ -26,14 +26,14 @@ module Flag
let b = ref 0 in
let i = ref 0 in
let r = ref n in
label Init:
'Init:
while !i < !r do
invariant { 0 <= !b <= !i <= !r <= n /\
monochrome a 0 !b Blue /\
monochrome a !b !i White /\
monochrome a !r n Red /\
length a = n /\
permut_sub a (at a Init) 0 n }
permut_sub a (at a 'Init) 0 n }
variant { !r - !i }
match a[!i] with
| Blue ->
......
......@@ -8,14 +8,14 @@ module M
let gcd (x:int) (y:int) =
{ x >= 0 /\ y >= 0 }
let x = ref x in let y = ref y in
label Pre:
'Pre:
let a = ref 1 in let b = ref 0 in
let c = ref 0 in let d = ref 1 in
while (!y > 0) do
invariant { !x >= 0 /\ !y >= 0 /\
(forall d:int. gcd !x !y d -> gcd (at !x Pre) (at !y Pre) d) /\
!a * (at !x Pre) + !b * (at !y Pre) = !x /\
!c * (at !x Pre) + !d * (at !y Pre) = !y }
(forall d:int. gcd !x !y d -> gcd (at !x 'Pre) (at !y 'Pre) d) /\
!a * (at !x 'Pre) + !b * (at !y 'Pre) = !x /\
!c * (at !x 'Pre) + !d * (at !y 'Pre) = !y }
variant { !y }
let r = mod !x !y in let q = div !x !y in
x := !y; y := r;
......
......@@ -12,22 +12,22 @@ module InsertionSort
let insertion_sort (a: array int) =
{ }
label L:
'L:
for i = 1 to length a - 1 do
(* a[0..i[ is sorted; now insert a[i] *)
invariant { sorted_sub a 0 i /\ permut a (at a L) }
invariant { sorted_sub a 0 i /\ permut a (at a 'L) }
let v = a[i] in
let j = ref i in
while !j > 0 && a[!j - 1] > v do
invariant {
0 <= !j <= i /\ permut a[!j <- v] (at a L) /\
0 <= !j <= i /\ permut a[!j <- v] (at a 'L) /\
(forall k1 k2: int.
0 <= k1 <= k2 <= i -> k1 <> !j -> k2 <> !j -> a[k1] <= a[k2]) /\
(forall k: int. !j+1 <= k <= i -> v < a[k]) }
variant { !j }
label L1:
'L1:
a[!j] <- a[!j - 1];
assert { exchange a[!j-1 <- v] (at a L1)[!j <- v] (!j - 1) !j};
assert { exchange a[!j-1 <- v] (at a 'L1)[!j <- v] (!j - 1) !j};
j := !j - 1
done;
assert { forall k: int. 0 <= k < !j -> a[k] <= v };
......
......@@ -330,11 +330,11 @@ module M2
let old_next = !next in
let old_p = !p in
let q = ref null in
label Init:
'Init:
while !p <> null do
invariant { is_list !next !p /\ is_list !next !q
/\ sep_list_list !next !p !q /\
reverse (model (at !next Init) (old_p)) =
reverse (model (at !next 'Init) (old_p)) =
(reverse (model !next !p)) ++ (model !next !q)}
let tmp = !next[!p] in
let bak_next = !next in
......
......@@ -81,7 +81,7 @@ exception Success
let search_safety () =
{ length x = m }
label Init:
'Init:
let s = ref 0 in
for i = 0 to m - 1 do (* could be n instead of m *)
s := !s + x[i]
......@@ -116,7 +116,7 @@ let search_safety () =
let search () =
{ length x = m /\ is_integer x.elts }
label Init:
'Init:
let s = ref 0 in
for i = 0 to m - 1 do (* could be n instead of m *)
invariant { !s = sum x.elts 0 i }
......@@ -125,11 +125,11 @@ let search () =
assert { !s = sum x.elts 0 m };
for d = 0 to m - 1 do
invariant {
x = at x Init /\
x = at x 'Init /\
!s = sum x.elts d m
}
for c = x[d] + 1 to 9 do
invariant { x = at x Init }
invariant { x = at x 'Init }
let delta = y - !s - c + x[d] in
if 0 <= delta && delta <= 9 * d then begin
x[d] <- c;
......@@ -240,7 +240,7 @@ let search_smallest () =
(* x has at most n digits *)
forall k : int. n <= k < m -> x[k] = 0
}
label Init:
'Init:
let s = ref 0 in
for i = 0 to m - 1 do (* could be n instead of m *)
invariant { !s = sum x.elts 0 i }
......@@ -249,24 +249,24 @@ let search_smallest () =
assert { !s = sum x.elts 0 m };
for d = 0 to m - 1 do
invariant {
x = at x Init /\
x = at x 'Init /\
!s = sum x.elts d m /\
forall u : int.
interp (at x.elts Init) 0 m < u <= interp9 x.elts d m -> sum_digits u <> y
interp (at x.elts 'Init) 0 m < u <= interp9 x.elts d m -> sum_digits u <> y
}
for c = x[d] + 1 to 9 do
invariant {
x = at x Init /\
x = at x 'Init /\
forall c' : int. x[d] < c' < c ->
forall u : int.
interp (at x.elts Init) 0 m < u <= interp9 (M.set x.elts d c') d m ->
interp (at x.elts 'Init) 0 m < u <= interp9 (M.set x.elts d c') d m ->
sum_digits u <> y }
let delta = y - !s - c + x[d] in
if 0 <= delta && delta <= 9 * d then begin
assert { smallest_size delta <= d };
x[d] <- c;
assert { sum x.elts d m = y - delta };
assert { gt_digit x.elts (at x.elts Init) d };
assert { gt_digit x.elts (at x.elts 'Init) d };
let k = div delta 9 in
assert { k <= d };
for i = 0 to d - 1 do
......@@ -277,7 +277,7 @@ let search_smallest () =
(forall j : int. 0 <= j < i ->
(j < smallest_size delta -> x[j] = M.get (smallest delta) j) /\
(j >= smallest_size delta -> x[j] = 0)) /\
gt_digit x.elts (at x.elts Init) d }
gt_digit x.elts (at x.elts 'Init) d }
if i < k then x[i] <- 9
else if i = k then x[i] <- mod delta 9
else x[i] <- 0;
......
......@@ -26,11 +26,11 @@ module Quicksort
if l < r then begin
let v = t[l] in
let m = ref l in
label L: begin
'L: begin
for i = l + 1 to r do
invariant { (forall j:int. l < j <= !m -> t[j] < v) /\
(forall j:int. !m < j < i -> t[j] >= v) /\
permut_sub t (at t L) l (r+1) /\
permut_sub t (at t 'L) l (r+1) /\
t[l] = v /\ l <= !m < i }
if t[i] < v then begin m := !m + 1; swap t i !m end
done;
......
......@@ -19,11 +19,11 @@ module Quicksort
let selection_sort (a: array int) =
{ }
label L:
'L:
for i = 0 to length a - 1 do
(* a[0..i[ is sorted; now find minimum of a[i..n[ *)
invariant
{ sorted_sub a 0 i /\ permut a (at a L) /\
{ sorted_sub a 0 i /\ permut a (at a 'L) /\
forall k1 k2: int. 0 <= k1 < i <= k2 < length a -> a[k1] <= a[k2] }
let min = ref i in
for j = i + 1 to length a - 1 do
......@@ -31,9 +31,9 @@ module Quicksort
{ i <= !min < j && forall k: int. i <= k < j -> a[!min] <= a[k] }
if a[j] < a[!min] then min := j
done;
label L1:
'L1:
if !min <> i then swap a !min i;
assert { permut a (at a L1) }
assert { permut a (at a 'L1) }
done
{ sorted a /\ permut a (old a) }
......
......@@ -15,9 +15,9 @@ module HoareLogic
let slow_subtraction (x: ref int) (z: ref int) =
{ !x >= 0 }
label Init:
'Init:
while !x <> 0 do
invariant { 0 <= !x /\ !z - !x = at !z Init - at !x Init } variant { !x }
invariant { 0 <= !x /\ !z - !x = at !z 'Init - at !x 'Init } variant { !x }
z := !z - 1;
x := !x - 1
done
......@@ -34,9 +34,9 @@ module HoareLogic
let slow_addition (x: ref int) (z: ref int) =
{ !x >= 0 }
label Init:
'Init:
while !x <> 0 do
invariant { 0 <= !x /\ !z + !x = at !z Init + at !x Init } variant { !x }
invariant { 0 <= !x /\ !z + !x = at !z 'Init + at !x 'Init } variant { !x }
z := !z + 1;
x := !x - 1
done
......@@ -53,10 +53,10 @@ module HoareLogic
let parity (x: ref int) (y: ref int) =
{ !x >= 0 }
y := 0;
label Init:
'Init:
while !x <> 0 do
invariant { 0 <= !x /\ (!y=0 /\ even (at !x Init - !x) \/
!y=1 /\ even (at !x Init - !x + 1)) }
invariant { 0 <= !x /\ (!y=0 /\ even (at !x 'Init - !x) \/
!y=1 /\ even (at !x 'Init - !x + 1)) }
variant { !x }
y := 1 - !y;
x := !x - 1
......@@ -112,10 +112,10 @@ module MoreHoareLogic
let list_sum (l: ref (list int)) (y: ref int) =
{}
y := 0;
label Init:
'Init:
while !l <> Nil do
invariant { length !l <= length (at !l Init) /\
!y + sum !l = sum (at !l Init) }
invariant { length !l <= length (at !l 'Init) /\
!y + sum !l = sum (at !l 'Init) }
variant { length !l }
y := !y + head !l;
l := tail !l
......@@ -129,12 +129,12 @@ module MoreHoareLogic
let list_member (x : ref (list 'a)) (y: 'a) (z: ref int) =
{}
z := 0;
label Init:
'Init:
while !x <> Nil do
invariant { length !x <= length (at !x Init) /\
(mem y !x -> mem y (at !x Init)) /\
(!z=1 /\ mem y (at !x Init) \/
!z=0 /\ (mem y (at !x Init) -> mem y !x)) }
invariant { length !x <= length (at !x 'Init) /\
(mem y !x -> mem y (at !x 'Init)) /\
(!z=1 /\ mem y (at !x 'Init) \/
!z=0 /\ (mem y (at !x 'Init) -> mem y !x)) }
variant { length !x }
if y = head !x then z := 1;
x := tail !x
......
......@@ -82,11 +82,11 @@ module NQueens
let rec bt_queens (board: array int) (n: int) (pos: int) variant { n - pos } =
{ length board = n /\ 0 <= pos <= n /\ solution board pos }
label Init:
'Init:
if pos = n then raise Solution;
for i = 0 to n - 1 do
invariant {
eq_board board (at board Init) pos /\
eq_board board (at board 'Init) pos /\
forall b:array int. length b = n -> is_board b n ->
eq_board board b pos -> 0 <= b[pos] < i -> not (solution b n) }
board[pos] <- i;
......
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