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
212a4d3b
Commit
212a4d3b
authored
May 15, 2015
by
Jean-Christophe Filliâtre
Browse files
gallery: simple verification exercises
parent
2036ffd2
Changes
3
Hide whitespace changes
Inline
Side-by-side
examples/swap.mlw
0 → 100644
View file @
212a4d3b
module Swap
use import int.Int
use import ref.Ref
let swap (a b: ref int) : unit
writes { a, b }
ensures { !a = old !b /\ !b = old !a }
=
a := !a + !b;
b := !a - !b;
a := !a - !b
end
examples/swap/why3session.xml
0 → 100644
View file @
212a4d3b
<?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"
/>
<file
name=
"../swap.mlw"
expanded=
"true"
>
<theory
name=
"Swap"
sum=
"5488140ff7d3e24ad9f42a3b571a28a3"
expanded=
"true"
>
<goal
name=
"WP_parameter swap"
expl=
"VC for swap"
expanded=
"true"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.01"
steps=
"3"
/></proof>
</goal>
</theory>
</file>
</why3session>
examples/swap/why3shapes.gz
0 → 100644
View file @
212a4d3b
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