Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
12bb1ee3
Commit
12bb1ee3
authored
May 23, 2017
by
MARCHE Claude
Browse files
Updated 3 more extraction examples, 1 more to go
parent
18a1ceff
Changes
11
Hide whitespace changes
Inline
Side-by-side
bench/bench
View file @
12bb1ee3
...
...
@@ -228,11 +228,11 @@ echo ""
echo
"=== Extraction to Ocaml ==="
extract_and_run examples/euler001 euler001.ml 1000000
extract_and_run examples/gcd gcd.ml 6 15
echo
"TODO: update 4 more extraction examples"
# extract_and_run examples/vstte10_max_sum vstte10_max_sum__*.ml
# extract_and_run examples/vstte12_combinators vstte12_combinators__*.ml "((((K K) K) K) K)"
extract_and_run examples/vstte10_max_sum vstte10_max_sum.ml
extract_and_run examples/vstte12_combinators vstte12_combinators.ml
"((((K K) K) K) K)"
extract_and_run examples/defunctionalization defunctionalization.ml
echo
"TODO: update 1 more extraction example"
# extract_and_run examples/sudoku sudoku__*.ml 2,0,9,0,0,0,0,1,0,0,0,0,0,6,0,0,0,0,0,5,3,8,0,2,7,0,0,3,0,0,0,0,0,0,0,0,0,0,0,0,7,5,0,0,3,0,4,1,2,0,8,9,0,0,0,0,4,0,9,0,0,2,0,8,0,0,0,0,1,0,0,5,0,0,0,0,0,0,0,7,6
# extract_and_run examples/defunctionalization defunctionalization__*.ml
echo
""
...
...
examples/defunctionalization.mlw
View file @
12bb1ee3
...
...
@@ -41,20 +41,15 @@ p4 = 10 - (2 - 3)
</pre></blockquote>}
*)
val constant p0 : prog
ensures { result = Cte 0 }
let constant p0 : prog = Cte 0
val constant p1 : prog
ensures { result = Sub (Cte 10) (Cte 6) }
let constant p1 : prog = Sub (Cte 10) (Cte 6)
val constant p2 : prog
ensures { result = Sub (Sub (Cte 10) (Cte 6)) (Sub (Cte 7) (Cte 2)) }
let constant p2 : prog = Sub (Sub (Cte 10) (Cte 6)) (Sub (Cte 7) (Cte 2))
val constant p3 : prog
ensures { result = Sub (Sub (Cte 7) (Cte 2)) (Sub (Cte 10) (Cte 6)) }
let constant p3 : prog = Sub (Sub (Cte 7) (Cte 2)) (Sub (Cte 10) (Cte 6))
val constant p4 : prog
ensures { result = Sub (Cte 10) (Sub (Cte 2) (Cte 3)) }
let constant p4 : prog = Sub (Cte 10) (Sub (Cte 2) (Cte 3))
end
...
...
@@ -152,23 +147,20 @@ use import Expr
*)
function eval_1 (e:expr) (k: int->'a) : 'a =
match e with
use import DirectSem
let rec eval_1 (e:expr) (k: int->'a) : 'a
variant { e }
ensures { result = k (eval_0 e) }
= match e with
| Cte n -> k n
| Sub e1 e2 ->
eval_1 e1 (fun v1 -> eval_1 e2 (fun v2 -> k (v1 - v2)))
end
function interpret_1 (p : prog) : int = eval_1 p (fun n -> n)
(** Soundness *)
use import DirectSem
lemma cps_correct_expr: forall e:expr, k: int->'a. eval_1 e k = k (eval_0 e)
lemma cps_correct: forall p. interpret_1 p = interpret_0 p
let interpret_1 (p : prog) : int
ensures { result = eval_0 p }
= eval_1 p (fun n -> n)
end
...
...
examples/defunctionalization/Makefile
View file @
12bb1ee3
...
...
@@ -22,11 +22,7 @@ endif
MAIN
=
main
OBJ
=
defunctionalization__Expr
\
defunctionalization__DirectSem
\
defunctionalization__CPS
\
defunctionalization__Defunctionalization
\
OBJ
=
defunctionalization
ML
=
$(
addsuffix
.ml,
$(OBJ)
)
CMO
=
$(
addsuffix
.cmo,
$(OBJ)
)
CMX
=
$(
addsuffix
.cmx,
$(OBJ)
)
...
...
@@ -51,7 +47,10 @@ $(MAIN).opt: $(CMX) $(MAIN).cmx
$(MAIN).cmx
:
$(CMX)
$(ML)
:
../defunctionalization.mlw
$(WHY3)
extract
-D
ocaml64 ../defunctionalization.mlw
-o
.
$(WHY3)
extract
-D
ocaml64
--recursive
-L
..
-o
$@
\
defunctionalization.DirectSem
\
defunctionalization.CPS
\
defunctionalization.Defunctionalization
%.cmx
:
%.ml
$(OCAMLOPT)
$(INCLUDE)
-annot
-c
$<
...
...
examples/defunctionalization/main.ml
View file @
12bb1ee3
...
...
@@ -11,17 +11,17 @@ let input =
if
Array
.
length
Sys
.
argv
<>
1
then
usage
()
open
Defunctionalization
__Expr
open
Defunctionalization
let
rec
p_expr
fmt
e
=
match
e
with
|
Cte
n
->
fprintf
fmt
"%s"
(
Why3__BigInt
.
to_string
n
)
|
Sub
(
e1
,
e2
)
->
|
Sub
(
e1
,
e2
)
->
fprintf
fmt
"(%a - %a)"
p_expr
e1
p_expr
e2
let
p_prog
fmt
p
=
p_expr
fmt
p
let
p_value
fmt
v
=
let
p_value
fmt
v
=
fprintf
fmt
"%s"
(
Why3__BigInt
.
to_string
v
)
let
run
s
f
p
=
...
...
@@ -30,36 +30,35 @@ let run s f p =
let
()
=
printf
"Exercise 0: direct semantics@."
;
let
i
=
Defunctionalization
__DirectSem
.
interpret_0
in
run
"interpret_0"
i
Defunctionalization
__Expr
.
p0
;
run
"interpret_0"
i
Defunctionalization
__Expr
.
p1
;
run
"interpret_0"
i
Defunctionalization
__Expr
.
p2
;
run
"interpret_0"
i
Defunctionalization
__Expr
.
p3
;
run
"interpret_0"
i
Defunctionalization
__Expr
.
p4
;
let
i
=
Defunctionalization
.
interpret_0
in
run
"interpret_0"
i
Defunctionalization
.
p0
;
run
"interpret_0"
i
Defunctionalization
.
p1
;
run
"interpret_0"
i
Defunctionalization
.
p2
;
run
"interpret_0"
i
Defunctionalization
.
p3
;
run
"interpret_0"
i
Defunctionalization
.
p4
;
printf
"Done.@
\n
@."
(* does not work because lambda is not extracted into OCaml
(* does not work because lambda is not extracted into OCaml
(fun ... -> ...)
*)
let
()
=
printf
"Exercise 1: CPS@."
;
let i = Defunctionalization
__CPS
.interpret_1 in
run "interpret_1" i Defunctionalization
__Expr
.p0;
run "interpret_1" i Defunctionalization
__Expr
.p1;
run "interpret_1" i Defunctionalization
__Expr
.p2;
run "interpret_1" i Defunctionalization
__Expr
.p3;
run "interpret_1" i Defunctionalization
__Expr
.p4;
let
i
=
Defunctionalization
.
interpret_1
in
run
"interpret_1"
i
Defunctionalization
.
p0
;
run
"interpret_1"
i
Defunctionalization
.
p1
;
run
"interpret_1"
i
Defunctionalization
.
p2
;
run
"interpret_1"
i
Defunctionalization
.
p3
;
run
"interpret_1"
i
Defunctionalization
.
p4
;
printf
"Done.@
\n
@."
*)
let
()
=
printf
"Exercise 2: Defunctionalization@."
;
let
i
=
Defunctionalization__
Defunctionalization
.
interpret_2
in
run
"interpret_2"
i
Defunctionalization
__Expr
.
p0
;
run
"interpret_2"
i
Defunctionalization
__Expr
.
p1
;
run
"interpret_2"
i
Defunctionalization
__Expr
.
p2
;
run
"interpret_2"
i
Defunctionalization
__Expr
.
p3
;
run
"interpret_2"
i
Defunctionalization
__Expr
.
p4
;
let
i
=
Defunctionalization
.
interpret_2
in
run
"interpret_2"
i
Defunctionalization
.
p0
;
run
"interpret_2"
i
Defunctionalization
.
p1
;
run
"interpret_2"
i
Defunctionalization
.
p2
;
run
"interpret_2"
i
Defunctionalization
.
p3
;
run
"interpret_2"
i
Defunctionalization
.
p4
;
printf
"Done.@
\n
@."
examples/defunctionalization/why3session.xml
View file @
12bb1ee3
...
...
@@ -2,7 +2,7 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session
shape_version=
"4"
>
<prover
id=
"0"
name=
"CVC3"
version=
"2.4.1"
timelimit=
"5"
steplimit=
"0"
memlimit=
"
4
000"
/>
<prover
id=
"0"
name=
"CVC3"
version=
"2.4.1"
timelimit=
"5"
steplimit=
"0"
memlimit=
"
1
000"
/>
<prover
id=
"1"
name=
"Z3"
version=
"4.3.1"
timelimit=
"5"
steplimit=
"0"
memlimit=
"1000"
/>
<prover
id=
"2"
name=
"Z3"
version=
"3.2"
timelimit=
"5"
steplimit=
"0"
memlimit=
"1000"
/>
<prover
id=
"3"
name=
"Alt-Ergo"
version=
"0.95.2"
timelimit=
"6"
steplimit=
"0"
memlimit=
"1000"
/>
...
...
@@ -40,28 +40,19 @@
<proof
prover=
"7"
><result
status=
"valid"
time=
"0.00"
steps=
"1"
/></proof>
</goal>
<goal
name=
"eval_p3"
>
<proof
prover=
"0"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"1"
memlimit=
"4000"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"2"
memlimit=
"4000"
><result
status=
"valid"
time=
"0.02"
/></proof>
<proof
prover=
"3"
timelimit=
"5"
><result
status=
"valid"
time=
"0.02"
steps=
"7"
/></proof>
<proof
prover=
"4"
memlimit=
"4000"
><result
status=
"valid"
time=
"0.01"
/></proof>
</goal>
</theory>
<theory
name=
"CPS"
sum=
"82b26c2ca649503f06c24e2173e94eca"
>
<goal
name=
"cps_correct_expr"
>
<transf
name=
"induction_ty_lex"
>
<goal
name=
"cps_correct_expr.1"
expl=
"1."
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.01"
steps=
"22"
/></proof>
</goal>
</transf>
<theory
name=
"CPS"
sum=
"fca777f79915177c4b0efbae84734823"
>
<goal
name=
"VC eval_1"
expl=
"VC for eval_1"
>
<proof
prover=
"7"
><result
status=
"valid"
time=
"0.01"
steps=
"46"
/></proof>
</goal>
<goal
name=
"cps_correct"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"1"
memlimit=
"4000"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"2"
memlimit=
"4000"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.01"
steps=
"3"
/></proof>
<proof
prover=
"4"
memlimit=
"4000"
><result
status=
"valid"
time=
"0.01"
/></proof>
<goal
name=
"VC interpret_1"
expl=
"VC for interpret_1"
>
<proof
prover=
"7"
><result
status=
"valid"
time=
"0.00"
steps=
"2"
/></proof>
</goal>
</theory>
<theory
name=
"Defunctionalization"
sum=
"f5bf46667f77325130e49decc8994e61"
>
...
...
@@ -119,17 +110,17 @@
<proof
prover=
"7"
><result
status=
"valid"
time=
"0.00"
steps=
"3"
/></proof>
</goal>
</theory>
<theory
name=
"SemWithError"
sum=
"b86f86d1abcb9f97e04b692072fcf03b"
expanded=
"true"
>
<goal
name=
"cps_correct_expr"
expanded=
"true"
>
<transf
name=
"induction_ty_lex"
expanded=
"true"
>
<goal
name=
"cps_correct_expr.1"
expl=
"1."
expanded=
"true"
>
<transf
name=
"split_goal_wp"
expanded=
"true"
>
<theory
name=
"SemWithError"
sum=
"b86f86d1abcb9f97e04b692072fcf03b"
>
<goal
name=
"cps_correct_expr"
>
<transf
name=
"induction_ty_lex"
>
<goal
name=
"cps_correct_expr.1"
expl=
"1."
>
<transf
name=
"split_goal_wp"
>
<goal
name=
"cps_correct_expr.1.1"
expl=
"1."
>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.02"
steps=
"8"
/></proof>
</goal>
<goal
name=
"cps_correct_expr.1.2"
expl=
"2."
expanded=
"true"
>
<transf
name=
"introduce_premises"
expanded=
"true"
>
<goal
name=
"cps_correct_expr.1.2.1"
expl=
"1."
expanded=
"true"
>
<goal
name=
"cps_correct_expr.1.2"
expl=
"2."
>
<transf
name=
"introduce_premises"
>
<goal
name=
"cps_correct_expr.1.2.1"
expl=
"1."
>
<proof
prover=
"8"
><result
status=
"valid"
time=
"0.84"
/></proof>
</goal>
</transf>
...
...
@@ -139,7 +130,7 @@
</transf>
</goal>
<goal
name=
"cps_correct"
>
<proof
prover=
"0"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"3"
timelimit=
"5"
><result
status=
"valid"
time=
"0.02"
steps=
"4"
/></proof>
...
...
examples/defunctionalization/why3shapes.gz
View file @
12bb1ee3
No preview for this file type
examples/vstte10_max_sum/Makefile
View file @
12bb1ee3
...
...
@@ -20,7 +20,7 @@ ifeq ($(BENCH),yes)
endif
MAIN
=
main
OBJ
=
vstte10_max_sum
__MaxAndSum2 vstte10_max_sum__TestCase
OBJ
=
vstte10_max_sum
ML
=
$(
addsuffix
.ml,
$(OBJ)
)
CMO
=
$(
addsuffix
.cmo,
$(OBJ)
)
...
...
@@ -45,7 +45,7 @@ $(MAIN).opt: $(CMX) $(MAIN).cmx
$(MAIN).cmx
:
$(CMX)
$(ML)
:
../vstte10_max_sum.mlw
$(WHY3)
extract
-D
ocaml
32 ../vstte10_max_sum.mlw
-o
.
$(WHY3)
extract
-D
ocaml
64
-o
$@
$^
%.cmx
:
%.ml
$(OCAMLOPT)
$(INCLUDE)
-annot
-c
$<
...
...
@@ -59,6 +59,3 @@ $(ML): ../vstte10_max_sum.mlw
clean
::
rm
-f
$(ML)
*
.cm[xio]
*
.o
*
.annot
$(MAIN)
.opt
$(MAIN)
.byte
rm
-f
why3__
*
.ml
*
vstte10_max_sum__
*
.ml
*
int__
*
.ml
*
examples/vstte10_max_sum/main.ml
View file @
12bb1ee3
...
...
@@ -3,6 +3,6 @@ open Why3extract
open
Format
let
()
=
let
(
s
,
m
)
=
Vstte10_max_sum
__TestCase
.
test
()
in
let
(
s
,
m
)
=
Vstte10_max_sum
.
test
()
in
printf
"sum=%s, max=%s@."
(
Why3__BigInt
.
to_string
s
)
(
Why3__BigInt
.
to_string
m
)
examples/vstte12_combinators/Makefile
View file @
12bb1ee3
...
...
@@ -20,7 +20,7 @@ ifeq ($(BENCH),yes)
endif
MAIN
=
main
GEN
=
vstte12_combinators
__Combinators
GEN
=
vstte12_combinators
OBJ
=
$(GEN)
parse
GENML
=
$(
addsuffix
.ml,
$(GEN)
)
...
...
@@ -44,7 +44,7 @@ $(MAIN).opt: $(CMX) $(MAIN).cmx
$(MAIN).cmx
:
$(CMX)
$(GENML)
:
../vstte12_combinators.mlw
$(WHY3)
extract
-D
ocaml
32 ../vstte12_combinators.mlw
-o
.
$(WHY3)
extract
-D
ocaml
64
-o
$@
$<
%.cmx
:
%.ml
$(OCAMLOPT)
$(INCLUDE)
-annot
-c
$<
...
...
examples/vstte12_combinators/main.ml
View file @
12bb1ee3
...
...
@@ -13,8 +13,8 @@ let input =
let
input_term
=
if
input
=
"go"
then
let
i
=
Vstte12_combinators
__Combinators
.
i
in
Vstte12_combinators
__Combinators
.
App
(
i
,
i
)
let
i
=
Vstte12_combinators
.
i
in
Vstte12_combinators
.
App
(
i
,
i
)
else
try
Parse
.
parse_term
input
with
_
->
...
...
@@ -24,6 +24,6 @@ let input_term =
end
let
()
=
let
a
=
Vstte12_combinators
__Combinators
.
reduction
input_term
in
let
a
=
Vstte12_combinators
.
reduction
input_term
in
printf
"The normal form of %a is %a@."
Parse
.
pr
input_term
Parse
.
pr
a
examples/vstte12_combinators/parse.ml
View file @
12bb1ee3
open
Format
open
Vstte12_combinators
__Combinators
open
Vstte12_combinators
let
rec
pr
fmt
t
=
match
t
with
...
...
@@ -14,7 +14,7 @@ let rec parse_term s i =
match
String
.
get
s
i
with
|
'
S'
->
S
,
i
+
1
|
'
K'
->
K
,
i
+
1
|
'
I'
->
Vstte12_combinators
__Combinators
.
i
,
i
+
1
|
'
I'
->
Vstte12_combinators
.
i
,
i
+
1
|
'
(
'
->
let
t1
,
i1
=
parse_term
s
(
i
+
1
)
in
begin
...
...
@@ -36,4 +36,3 @@ let parse_term s =
if
i
<>
String
.
length
s
then
raise
SyntaxError
;
t
with
_
->
raise
SyntaxError
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new 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