Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
ee84cff8
Commit
ee84cff8
authored
May 04, 2015
by
Jean-Christophe Filliâtre
Browse files
new example: Dirichlet's principle (aka Pigeon holes)
parent
5c906623
Changes
3
Hide whitespace changes
Inline
Side-by-side
examples/dirichlet.mlw
0 → 100644
View file @
ee84cff8
(** Pigeon hole principle (also know as Dirichlet's principle)
proved using a lemma function. *)
module Dirichlet
use import HighOrd
use import int.Int
use import set.Fset
use import ref.Ref
exception Exit
let rec below (n: int) : set int
requires { 0 <= n }
ensures { forall i. mem i result <-> 0 <= i < n }
ensures { cardinal result = n }
variant { n }
= if n = 0 then empty else add (n-1) (below (n-1))
let lemma dirichlet (n m: int) (f: int -> int)
requires { 0 <= m < n }
requires { forall i. 0 <= i < n -> 0 <= f i < m }
ensures { exists i1, i2. 0 <= i1 < i2 < n /\ f i1 = f i2 }
=
let s = ref empty in
try
for i = 0 to n-1 do
invariant { cardinal !s = i }
invariant { forall x. mem x !s <-> (exists j. 0 <= j < i /\ x = f j) }
if mem (f i) !s then raise Exit;
s := add (f i) !s
done;
let b = below m in assert { subset !s b };
absurd
with Exit -> () end
end
examples/dirichlet/why3session.xml
0 → 100644
View file @
ee84cff8
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session
shape_version=
"4"
>
<prover
id=
"0"
name=
"Alt-Ergo"
version=
"0.99.1"
timelimit=
"6"
memlimit=
"1000"
/>
<prover
id=
"6"
name=
"Alt-Ergo"
version=
"0.95.1"
timelimit=
"6"
memlimit=
"1000"
/>
<file
name=
"../dirichlet.mlw"
expanded=
"true"
>
<theory
name=
"Dirichlet"
sum=
"8ee565a294b83da869ffcfd8fb11b973"
expanded=
"true"
>
<goal
name=
"WP_parameter below"
expl=
"VC for below"
expanded=
"true"
>
<proof
prover=
"6"
><result
status=
"valid"
time=
"0.01"
steps=
"75"
/></proof>
</goal>
<goal
name=
"WP_parameter dirichlet"
expl=
"VC for dirichlet"
expanded=
"true"
>
<transf
name=
"split_goal_wp"
expanded=
"true"
>
<goal
name=
"WP_parameter dirichlet.1"
expl=
"1. precondition"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.02"
steps=
"3"
/></proof>
</goal>
<goal
name=
"WP_parameter dirichlet.2"
expl=
"2. assertion"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.01"
steps=
"4"
/></proof>
</goal>
<goal
name=
"WP_parameter dirichlet.3"
expl=
"3. unreachable point"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.02"
steps=
"5"
/></proof>
</goal>
<goal
name=
"WP_parameter dirichlet.4"
expl=
"4. loop invariant init"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.01"
steps=
"7"
/></proof>
</goal>
<goal
name=
"WP_parameter dirichlet.5"
expl=
"5. loop invariant init"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.01"
steps=
"8"
/></proof>
</goal>
<goal
name=
"WP_parameter dirichlet.6"
expl=
"6. postcondition"
>
<proof
prover=
"6"
><result
status=
"valid"
time=
"0.02"
steps=
"22"
/></proof>
</goal>
<goal
name=
"WP_parameter dirichlet.7"
expl=
"7. loop invariant preservation"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.01"
steps=
"11"
/></proof>
</goal>
<goal
name=
"WP_parameter dirichlet.8"
expl=
"8. loop invariant preservation"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.02"
steps=
"53"
/></proof>
</goal>
<goal
name=
"WP_parameter dirichlet.9"
expl=
"9. precondition"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.00"
steps=
"5"
/></proof>
</goal>
<goal
name=
"WP_parameter dirichlet.10"
expl=
"10. assertion"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.02"
steps=
"28"
/></proof>
</goal>
<goal
name=
"WP_parameter dirichlet.11"
expl=
"11. unreachable point"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.01"
steps=
"9"
/></proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
examples/dirichlet/why3shapes.gz
0 → 100644
View file @
ee84cff8
File added
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment