Commit 6a36c00a authored by Guillaume Melquiond's avatar Guillaume Melquiond

Use why3doc comments rather than why3 label for module documentation.

parent 5e8735b3
......@@ -31,7 +31,7 @@ end
- an evaluation stack, containing integers.
*)
theory Vm "Virtual Machine for IMP language"
theory Vm
use import state.State
use import int.Int
......
......@@ -9,7 +9,9 @@ be:
By considering the terms in the Fibonacci sequence whose values do not
exceed four million, find the sum of the even-valued terms. *)
theory FibSumEven "sum of even-valued Fibonacci numbers"
(** {2 Sum of even-valued Fibonacci numbers} *)
theory FibSumEven
use import int.Int
use import int.Fibonacci
......
......@@ -31,7 +31,9 @@ module FibonacciLinear
end
module FibRecGhost "recursive version, using ghost code"
(** {2 Recursive version, using ghost code} *)
module FibRecGhost
use import int.Fibonacci
use import int.Int
......@@ -57,7 +59,9 @@ module FibRecGhost "recursive version, using ghost code"
end
module FibRecNoGhost "recursive version, without ghost code"
(** {2 Recursive version, without ghost code} *)
module FibRecNoGhost
use import int.Fibonacci
use import int.Int
......@@ -257,7 +261,9 @@ module Zeckendorf
end
theory Mat22 "2x2 integer matrices"
(** {2 2x2 integer matrices} *)
theory Mat22
use import int.Int
......
......@@ -23,7 +23,9 @@ theory Hyps
end
module Induction1 "with a simple induction"
(** {2 With a simple induction} *)
module Induction1
use import Hyps
predicate pr (k: int) = p k && p (k+1)
......@@ -34,7 +36,9 @@ module Induction1 "with a simple induction"
end
module Induction2 "with a strong induction"
(** {2 With a strong induction} *)
module Induction2
use import Hyps
clone import int.Induction
......@@ -44,7 +48,9 @@ module Induction2 "with a strong induction"
end
module LemmaFunction1 "with a recursive lemma function"
(** {2 With a recursive lemma function} *)
module LemmaFunction1
use import Hyps
let rec lemma ind (n: int) requires { 0 <= n} ensures { p n }
......@@ -57,7 +63,9 @@ module LemmaFunction1 "with a recursive lemma function"
end
module LemmaFunction2 "with a while loop"
(** {2 With a while loop} *)
module LemmaFunction2
use import Hyps
use import ref.Ref
......@@ -73,7 +81,9 @@ module LemmaFunction2 "with a while loop"
end
module LemmaFunction3 "with an ascending while loop"
(** {2 With an ascending while loop} *)
module LemmaFunction3
use import Hyps
use import ref.Ref
......
......@@ -18,8 +18,12 @@ theory Bijection
axiom Of_to : forall y : u. of (to_ y) = y
end
theory Einstein "Einstein's problem"
(** {2 Einstein's problem} *)
theory Einstein
(** Types *)
type house = H1 | H2 | H3 | H4 | H5
type color = Blue | Green | Red | White | Yellow
type person = Dane | Englishman | German | Norwegian | Swede
......@@ -28,15 +32,18 @@ theory Einstein "Einstein's problem"
type pet = Birds | Cats | Dogs | Fish | Horse
(** Each house is associated bijectively to a color and a person *)
clone Bijection as Color with type t = house, type u = color
clone Bijection as Owner with type t = house, type u = person
(** Each drink, cigar brand and pet are associated bijectively to a person *)
clone Bijection as Drink with type t = person, type u = drink
clone Bijection as Cigar with type t = person, type u = cigar
clone Bijection as Pet with type t = person, type u = pet
(** Relative positions of the houses *)
predicate leftof (h1 h2 : house) =
match h1, h2 with
| H1, H2
......@@ -105,7 +112,9 @@ theory Einstein "Einstein's problem"
end
theory Goals "Goals about Einstein's problem"
(** {2 Goals about Einstein's problem} *)
theory Goals
use import Einstein
(*
......
theory HelloProof "My very first Why3 theory"
theory HelloProof
goal G1 : true
......
(*
(** {1 The Scottish private club puzzle} *)
The classical example of the Scottish private club puzzle
(* The club follows six rules:
The club follows six rules:
- every non-scotti``sh members wear red socks
- every non-scottish members wear red socks
- every member wears a kilt or doesn't wear socks
......@@ -16,11 +14,11 @@ The club follows six rules:
- every scottish member wears a kilt
Problem: prove that there is nobody in this club !
Problem: prove that there is nobody in this club!
*)
theory ScottishClubProblem "the Scottish private club puzzle"
theory ScottishClubProblem
predicate is_scottish
predicate wears_red_socks
......
......@@ -19,7 +19,7 @@
maximum and memo).
*)
theory Bitset "sets of small integers"
theory Bitset
use import int.Int
......
......@@ -134,7 +134,9 @@ module BitsSpec
ensures { result.mdl = interval 0 (BV32.t'int n) }
end
module Bits "the 1-bits of an integer, as a set of integers"
(** {2 The 1-bits of an integer, as a set of integers} *)
module Bits
use import S
use import bv.BV32
......
......@@ -66,9 +66,11 @@ module Quicksort
end
(** {2 Knuth' shuffle} *)
(* a realistic quicksort first shuffles the array *)
module Shuffle "Knuth shuffle"
module Shuffle
use import int.Int
use import array.Array
......
......@@ -5,7 +5,7 @@
c+d)/2));return f;}main(q){scanf("%d",&q);printf("%d\n",t(~(~0<<q),0,0));}
*)
theory S "finite sets of with succ and pred operations"
theory S
use export set.Fsetint
......
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