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
8a28f1b1
Commit
8a28f1b1
authored
Sep 18, 2014
by
Léon Gondelman
Browse files
mini-compiler: clean-up (removed all but one coq proofs)
parent
9ca92458
Changes
19
Expand all
Hide whitespace changes
Inline
Side-by-side
examples/in_progress/mini-compiler/compiler.mlw
View file @
8a28f1b1
...
...
@@ -3,6 +3,7 @@
(*Imp to ImpVm compiler *)
(**************************************************************************)
module Compile_aexpr
meta compute_max_steps 0x10000
...
...
@@ -22,14 +23,16 @@ module Compile_aexpr
| VMS _ s m -> ms' = VMS (p + len) (push (aeval m a ) s) m
end
lemma aexpr_post_lemma:
meta rewrite_def function aexpr_post
(* lemma aexpr_post_lemma:
forall a len, x: 'a, p ms ms'.
aexpr_post a len x p ms ms' =
match ms with
| VMS _ s m -> ms' = VMS (p + len) (push (aeval m a ) s) m
end
meta rewrite prop aexpr_post_lemma
meta rewrite prop aexpr_post_lemma
*)
let rec compile_aexpr (a : aexpr) : hl 'a
...
...
@@ -61,7 +64,6 @@ module Compile_aexpr
end
module Compile_bexpr
use import int.Int
use import list.List
use import list.Length
...
...
@@ -139,7 +141,7 @@ end
module Compile_com
meta compute_max_steps 65536
use import int.Int
use import list.List
use import list.Length
...
...
@@ -157,11 +159,13 @@ module Compile_com
function com_pre (cmd: com) : 'a -> pos -> pred =
\x p ms. match ms with VMS p' _ m -> p = p' /\ exists m'. ceval m cmd m' end
lemma com_pre_lemma:
meta rewrite_def function com_pre
(*lemma com_pre_lemma:
forall cmd, x:'a, p ms. com_pre cmd x p ms =
match ms with VMS p' _ m -> p = p' /\ exists m'. ceval m cmd m' end
meta rewrite prop com_pre_lemma
meta rewrite prop com_pre_lemma
*)
function com_post (cmd: com) (len:pos) : 'a -> pos -> post =
\x p ms ms'. match ms, ms' with
...
...
@@ -169,14 +173,16 @@ module Compile_com
p' = p + len /\ s' = s /\ ceval m cmd m'
end
lemma com_post_lemma:
meta rewrite_def function com_post
(*lemma com_post_lemma:
forall cmd len, x:'a, p ms ms'. com_post cmd len x p ms ms' =
match ms, ms' with
| VMS p s m, VMS p' s' m' ->
p' = p + len /\ s' = s /\ ceval m cmd m'
end
meta rewrite prop com_post_lemma
meta rewrite prop com_post_lemma
*)
function exn_bool_old (b1: bexpr) (cond: bool) : ('a,machine_state) -> pos -> pred =
\x p ms. match snd x with
...
...
@@ -260,7 +266,10 @@ module Compile_com
(VMS p s m)
(VMS (p + length result) s m') }
= let res = compile_com com : hl unit in
assert { forall p s m m'. ceval m com m' -> res.pre () p (VMS p s m) };
assert {
forall c p s m m'. ceval m com m' -> codeseq_at c p res.code ->
res.pre () p (VMS p s m) && (forall ms'. res.post () p (VMS p s m) ms' ->
ms' = VMS (p + length res.code) s m')};
res.code
...
...
examples/in_progress/mini-compiler/compiler/compiler_Compile_com_WP_parameter_compile_com_natural_1.v
deleted
100644 → 0
View file @
9ca92458
This diff is collapsed.
Click to expand it.
examples/in_progress/mini-compiler/compiler/compiler_Compile_com_WP_parameter_compile_com_natural_2.v
deleted
100644 → 0
View file @
9ca92458
(
*
This
file
is
generated
by
Why3
'
s
Coq
driver
*
)
(
*
Beware
!
Only
edit
allowed
sections
below
*
)
Require
Import
BuiltIn
.
Require
BuiltIn
.
Require
int
.
Int
.
Require
int
.
Abs
.
Require
int
.
EuclideanDivision
.
Require
list
.
List
.
Require
list
.
Length
.
Require
list
.
Mem
.
Require
map
.
Map
.
Require
bool
.
Bool
.
Require
list
.
Append
.
Axiom
map
:
forall
(
a
:
Type
)
(
b
:
Type
),
Type
.
Parameter
map_WhyType
:
forall
(
a
:
Type
)
{
a_WT
:
WhyType
a
}
(
b
:
Type
)
{
b_WT
:
WhyType
b
}
,
WhyType
(
map
a
b
).
Existing
Instance
map_WhyType
.
Parameter
get
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
{
b
:
Type
}
{
b_WT
:
WhyType
b
}
,
(
map
a
b
)
->
a
->
b
.
Parameter
set
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
{
b
:
Type
}
{
b_WT
:
WhyType
b
}
,
(
map
a
b
)
->
a
->
b
->
(
map
a
b
).
Parameter
const
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
{
b
:
Type
}
{
b_WT
:
WhyType
b
}
,
b
->
(
map
a
b
).
(
*
Why3
assumption
*
)
Inductive
id
:=
|
Id
:
Z
->
id
.
Axiom
id_WhyType
:
WhyType
id
.
Existing
Instance
id_WhyType
.
(
*
Why3
assumption
*
)
Inductive
aexpr
:=
|
Anum
:
Z
->
aexpr
|
Avar
:
id
->
aexpr
|
Aadd
:
aexpr
->
aexpr
->
aexpr
|
Asub
:
aexpr
->
aexpr
->
aexpr
|
Amul
:
aexpr
->
aexpr
->
aexpr
.
Axiom
aexpr_WhyType
:
WhyType
aexpr
.
Existing
Instance
aexpr_WhyType
.
(
*
Why3
assumption
*
)
Inductive
bexpr
:=
|
Btrue
:
bexpr
|
Bfalse
:
bexpr
|
Band
:
bexpr
->
bexpr
->
bexpr
|
Bnot
:
bexpr
->
bexpr
|
Beq
:
aexpr
->
aexpr
->
bexpr
|
Ble
:
aexpr
->
aexpr
->
bexpr
.
Axiom
bexpr_WhyType
:
WhyType
bexpr
.
Existing
Instance
bexpr_WhyType
.
(
*
Why3
assumption
*
)
Inductive
com
:=
|
Cskip
:
com
|
Cassign
:
id
->
aexpr
->
com
|
Cseq
:
com
->
com
->
com
|
Cif
:
bexpr
->
com
->
com
->
com
|
Cwhile
:
bexpr
->
com
->
com
.
Axiom
com_WhyType
:
WhyType
com
.
Existing
Instance
com_WhyType
.
(
*
Why3
assumption
*
)
Fixpoint
aeval
(
st
:
(
map
id
Z
))
(
e
:
aexpr
)
{
struct
e
}:
Z
:=
match
e
with
|
(
Anum
n
)
=>
n
|
(
Avar
x
)
=>
(
get
st
x
)
|
(
Aadd
e1
e2
)
=>
((
aeval
st
e1
)
+
(
aeval
st
e2
))
%
Z
|
(
Asub
e1
e2
)
=>
((
aeval
st
e1
)
-
(
aeval
st
e2
))
%
Z
|
(
Amul
e1
e2
)
=>
((
aeval
st
e1
)
*
(
aeval
st
e2
))
%
Z
end
.
Parameter
beval
:
(
map
id
Z
)
->
bexpr
->
bool
.
Axiom
beval_def
:
forall
(
st
:
(
map
id
Z
))
(
b
:
bexpr
),
match
b
with
|
Btrue
=>
((
beval
st
b
)
=
true
)
|
Bfalse
=>
((
beval
st
b
)
=
false
)
|
(
Bnot
b
'
)
=>
((
beval
st
b
)
=
(
Init
.
Datatypes
.
negb
(
beval
st
b
'
)))
|
(
Band
b1
b2
)
=>
((
beval
st
b
)
=
(
Init
.
Datatypes
.
andb
(
beval
st
b1
)
(
beval
st
b2
)))
|
(
Beq
a1
a2
)
=>
(((
aeval
st
a1
)
=
(
aeval
st
a2
))
->
((
beval
st
b
)
=
true
))
/
\
((
~
((
aeval
st
a1
)
=
(
aeval
st
a2
)))
->
((
beval
st
b
)
=
false
))
|
(
Ble
a1
a2
)
=>
(((
aeval
st
a1
)
<=
(
aeval
st
a2
))
%
Z
->
((
beval
st
b
)
=
true
))
/
\
((
~
((
aeval
st
a1
)
<=
(
aeval
st
a2
))
%
Z
)
->
((
beval
st
b
)
=
false
))
end
.
(
*
Why3
assumption
*
)
Inductive
ceval
:
(
map
id
Z
)
->
com
->
(
map
id
Z
)
->
Prop
:=
|
E_Skip
:
forall
(
m
:
(
map
id
Z
)),
(
ceval
m
Cskip
m
)
|
E_Ass
:
forall
(
m
:
(
map
id
Z
))
(
a
:
aexpr
)
(
n
:
Z
)
(
x
:
id
),
((
aeval
m
a
)
=
n
)
->
(
ceval
m
(
Cassign
x
a
)
(
set
m
x
n
))
|
E_Seq
:
forall
(
cmd1
:
com
)
(
cmd2
:
com
)
(
m0
:
(
map
id
Z
))
(
m1
:
(
map
id
Z
))
(
m2
:
(
map
id
Z
)),
(
ceval
m0
cmd1
m1
)
->
((
ceval
m1
cmd2
m2
)
->
(
ceval
m0
(
Cseq
cmd1
cmd2
)
m2
))
|
E_IfTrue
:
forall
(
m0
:
(
map
id
Z
))
(
m1
:
(
map
id
Z
))
(
cond
:
bexpr
)
(
cmd1
:
com
)
(
cmd2
:
com
),
((
beval
m0
cond
)
=
true
)
->
((
ceval
m0
cmd1
m1
)
->
(
ceval
m0
(
Cif
cond
cmd1
cmd2
)
m1
))
|
E_IfFalse
:
forall
(
m0
:
(
map
id
Z
))
(
m1
:
(
map
id
Z
))
(
cond
:
bexpr
)
(
cmd1
:
com
)
(
cmd2
:
com
),
((
beval
m0
cond
)
=
false
)
->
((
ceval
m0
cmd2
m1
)
->
(
ceval
m0
(
Cif
cond
cmd1
cmd2
)
m1
))
|
E_WhileEnd
:
forall
(
cond
:
bexpr
)
(
m
:
(
map
id
Z
))
(
body
:
com
),
((
beval
m
cond
)
=
false
)
->
(
ceval
m
(
Cwhile
cond
body
)
m
)
|
E_WhileLoop
:
forall
(
mi
:
(
map
id
Z
))
(
mj
:
(
map
id
Z
))
(
mf
:
(
map
id
Z
))
(
cond
:
bexpr
)
(
body
:
com
),
((
beval
mi
cond
)
=
true
)
->
((
ceval
mi
body
mj
)
->
((
ceval
mj
(
Cwhile
cond
body
)
mf
)
->
(
ceval
mi
(
Cwhile
cond
body
)
mf
))).
Axiom
ceval_deterministic
:
forall
(
c
:
com
)
(
mi
:
(
map
id
Z
))
(
mf1
:
(
map
id
Z
))
(
mf2
:
(
map
id
Z
)),
(
ceval
mi
c
mf1
)
->
((
ceval
mi
c
mf2
)
->
(
mf1
=
mf2
)).
(
*
Why3
assumption
*
)
Inductive
machine_state
:=
|
VMS
:
Z
->
(
list
Z
)
->
(
map
id
Z
)
->
machine_state
.
Axiom
machine_state_WhyType
:
WhyType
machine_state
.
Existing
Instance
machine_state_WhyType
.
(
*
Why3
assumption
*
)
Inductive
instr
:=
|
Iconst
:
Z
->
instr
|
Ivar
:
id
->
instr
|
Isetvar
:
id
->
instr
|
Ibranch
:
Z
->
instr
|
Iadd
:
instr
|
Isub
:
instr
|
Imul
:
instr
|
Ibeq
:
Z
->
instr
|
Ibne
:
Z
->
instr
|
Ible
:
Z
->
instr
|
Ibgt
:
Z
->
instr
|
Ihalt
:
instr
.
Axiom
instr_WhyType
:
WhyType
instr
.
Existing
Instance
instr_WhyType
.
(
*
Why3
assumption
*
)
Inductive
codeseq_at
:
(
list
instr
)
->
Z
->
(
list
instr
)
->
Prop
:=
|
codeseq_at_intro
:
forall
(
c1
:
(
list
instr
))
(
c2
:
(
list
instr
))
(
c3
:
(
list
instr
))
(
pc
:
Z
),
(
pc
=
(
list
.
Length
.
length
c1
))
->
(
codeseq_at
(
Init
.
Datatypes
.
app
(
Init
.
Datatypes
.
app
c1
c2
)
c3
)
pc
c2
).
Parameter
transition_star
:
(
list
instr
)
->
machine_state
->
machine_state
->
Prop
.
Axiom
func
:
forall
(
a
:
Type
)
(
b
:
Type
),
Type
.
Parameter
func_WhyType
:
forall
(
a
:
Type
)
{
a_WT
:
WhyType
a
}
(
b
:
Type
)
{
b_WT
:
WhyType
b
}
,
WhyType
(
func
a
b
).
Existing
Instance
func_WhyType
.
Parameter
infix_at
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
{
b
:
Type
}
{
b_WT
:
WhyType
b
}
,
(
func
a
b
)
->
a
->
b
.
(
*
Why3
assumption
*
)
Inductive
hl
(
a
:
Type
)
:=
|
mk_hl
:
(
list
instr
)
->
(
func
a
(
func
Z
(
func
machine_state
bool
)))
->
(
func
a
(
func
Z
(
func
machine_state
(
func
machine_state
bool
))))
->
hl
a
.
Axiom
hl_WhyType
:
forall
(
a
:
Type
)
{
a_WT
:
WhyType
a
}
,
WhyType
(
hl
a
).
Existing
Instance
hl_WhyType
.
Implicit
Arguments
mk_hl
[[
a
]].
(
*
Why3
assumption
*
)
Definition
post
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
(
v
:
(
hl
a
))
:
(
func
a
(
func
Z
(
func
machine_state
(
func
machine_state
bool
))))
:=
match
v
with
|
(
mk_hl
x
x1
x2
)
=>
x2
end
.
(
*
Why3
assumption
*
)
Definition
pre
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
(
v
:
(
hl
a
))
:
(
func
a
(
func
Z
(
func
machine_state
bool
)))
:=
match
v
with
|
(
mk_hl
x
x1
x2
)
=>
x1
end
.
(
*
Why3
assumption
*
)
Definition
code
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
(
v
:
(
hl
a
))
:
(
list
instr
)
:=
match
v
with
|
(
mk_hl
x
x1
x2
)
=>
x
end
.
(
*
Why3
assumption
*
)
Definition
contextual_irrelevance
(
c
:
(
list
instr
))
(
p
:
Z
)
(
ms1
:
machine_state
)
(
ms2
:
machine_state
)
:
Prop
:=
forall
(
c_global
:
(
list
instr
)),
(
codeseq_at
c_global
p
c
)
->
(
transition_star
c_global
ms1
ms2
).
(
*
Why3
assumption
*
)
Definition
hl_correctness
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
(
cs
:
(
hl
a
))
:
Prop
:=
forall
(
x
:
a
)
(
p
:
Z
)
(
ms
:
machine_state
),
((
infix_at
(
infix_at
(
infix_at
(
pre
cs
)
x
)
p
)
ms
)
=
true
)
->
exists
ms
'
:
machine_state
,
((
infix_at
(
infix_at
(
infix_at
(
infix_at
(
post
cs
)
x
)
p
)
ms
)
ms
'
)
=
true
)
/
\
(
contextual_irrelevance
(
code
cs
)
p
ms
ms
'
).
Parameter
com_pre
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
com
->
(
func
a
(
func
Z
(
func
machine_state
bool
))).
Axiom
com_pre_def
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
cmd
:
com
)
(
x
:
a
)
(
p
:
Z
)
(
ms
:
machine_state
),
((
infix_at
(
infix_at
(
infix_at
(
com_pre
cmd
:
(
func
a
(
func
Z
(
func
machine_state
bool
))))
x
)
p
)
ms
)
=
true
)
<->
match
ms
with
|
(
VMS
p
'
_
m
)
=>
(
p
=
p
'
)
/
\
exists
m
'
:
(
map
id
Z
),
(
ceval
m
cmd
m
'
)
end
.
Parameter
com_post
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
com
->
Z
->
(
func
a
(
func
Z
(
func
machine_state
(
func
machine_state
bool
)))).
Axiom
com_post_def
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
cmd
:
com
)
(
len
:
Z
)
(
x
:
a
)
(
p
:
Z
)
(
ms
:
machine_state
)
(
ms
'
:
machine_state
),
((
infix_at
(
infix_at
(
infix_at
(
infix_at
(
com_post
cmd
len
:
(
func
a
(
func
Z
(
func
machine_state
(
func
machine_state
bool
)))))
x
)
p
)
ms
)
ms
'
)
=
true
)
<->
match
(
ms
,
ms
'
)
with
|
((
VMS
p1
s
m
),
(
VMS
p
'
s
'
m
'
))
=>
(
p
'
=
(
p1
+
len
)
%
Z
)
/
\
((
s
'
=
s
)
/
\
(
ceval
m
cmd
m
'
))
end
.
(
*
Why3
goal
*
)
Theorem
WP_parameter_compile_com_natural
:
forall
(
com1
:
com
),
forall
(
res
:
(
list
instr
))
(
res1
:
(
func
unit
(
func
Z
(
func
machine_state
bool
))))
(
res2
:
(
func
unit
(
func
Z
(
func
machine_state
(
func
machine_state
bool
))))),
((
res1
=
(
com_pre
com1
:
(
func
unit
(
func
Z
(
func
machine_state
bool
)))))
/
\
((
res2
=
(
com_post
com1
(
list
.
Length
.
length
res
)
:
(
func
unit
(
func
Z
(
func
machine_state
(
func
machine_state
bool
))))))
/
\
(
hl_correctness
(
mk_hl
res
res1
res2
))))
->
((
forall
(
p
:
Z
)
(
s
:
(
list
Z
))
(
m
:
(
map
id
Z
))
(
m
'
:
(
map
id
Z
)),
(
ceval
m
com1
m
'
)
->
((
infix_at
(
infix_at
(
infix_at
res1
tt
)
p
)
(
VMS
p
s
m
))
=
true
))
->
forall
(
c
:
(
list
instr
))
(
p
:
Z
)
(
s
:
(
list
Z
))
(
m
:
(
map
id
Z
))
(
m
'
:
(
map
id
Z
)),
(
ceval
m
com1
m
'
)
->
((
codeseq_at
c
p
res
)
->
(
transition_star
c
(
VMS
p
s
m
)
(
VMS
(
p
+
(
list
.
Length
.
length
res
))
%
Z
s
m
'
)))).
(
*
Why3
intros
com1
res
res1
res2
(
h1
,(
h2
,
h3
))
h4
c
p
s
m
m
'
h5
h6
.
*
)
intros
com1
res
res1
res2
(
h1
,(
h2
,
h3
))
h4
c
p
s
m
m
'
h5
h6
.
unfold
hl_correctness
in
*
.
remember
h5
as
h7
eqn
:
eqn
;
clear
eqn
.
apply
(
h4
p
s
)
in
h5
.
apply
h3
in
h5
.
Require
Import
Why3
.
simpl
in
*
.
subst
.
destruct
h5
.
rewrite
com_post_def
in
H
.
why3
"Alt-Ergo,0.95.2,"
.
Qed
.
examples/in_progress/mini-compiler/compiler/why3session.xml
View file @
8a28f1b1
This diff is collapsed.
Click to expand it.
examples/in_progress/mini-compiler/compiler/why3shapes.gz
View file @
8a28f1b1
No preview for this file type
examples/in_progress/mini-compiler/imp.why
View file @
8a28f1b1
...
...
@@ -51,13 +51,13 @@ theory Imp
if (aeval st a1) <= (aeval st a2) then True else False
end
lemma inversion_beval_t :
(*
lemma inversion_beval_t :
forall a1 a2: aexpr, m: state.
beval m (Beq a1 a2) = True -> aeval m a1 = aeval m a2
lemma inversion_beval_f :
forall a1 a2: aexpr, m: state.
beval m (Beq a1 a2) = False -> aeval m a1 <> aeval m a2
beval m (Beq a1 a2) = False -> aeval m a1 <> aeval m a2
*)
inductive ceval state com state =
(* skip *)
...
...
@@ -104,7 +104,9 @@ theory Imp
ceval mi (Cwhile cond body) mf
lemma ceval_deterministic:
forall c mi mf1
mf2
. ceval mi c mf1 -> ceval mi c mf2 -> mf1 = mf2
lemma ceval_deterministic
_aux
:
forall c mi mf1. ceval mi c mf1 ->
forall mf2. ("inversion"
ceval mi c mf2
)
-> mf1 = mf2
lemma ceval_deterministic :
forall c mi mf1 mf2. ceval mi c mf1 -> ceval mi c mf2 -> mf1 = mf2
end
\ No newline at end of file
examples/in_progress/mini-compiler/imp/imp_Imp_ceval_deterministic_1.v
deleted
100644 → 0
View file @
9ca92458
(
*
This
file
is
generated
by
Why3
'
s
Coq
driver
*
)
(
*
Beware
!
Only
edit
allowed
sections
below
*
)
Require
Import
BuiltIn
.
Require
BuiltIn
.
Require
map
.
Map
.
Require
int
.
Int
.
Require
bool
.
Bool
.
Axiom
map
:
forall
(
a
:
Type
)
(
b
:
Type
),
Type
.
Parameter
map_WhyType
:
forall
(
a
:
Type
)
{
a_WT
:
WhyType
a
}
(
b
:
Type
)
{
b_WT
:
WhyType
b
}
,
WhyType
(
map
a
b
).
Existing
Instance
map_WhyType
.
Parameter
get
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
{
b
:
Type
}
{
b_WT
:
WhyType
b
}
,
(
map
a
b
)
->
a
->
b
.
Parameter
set
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
{
b
:
Type
}
{
b_WT
:
WhyType
b
}
,
(
map
a
b
)
->
a
->
b
->
(
map
a
b
).
Axiom
Select_eq
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
{
b
:
Type
}
{
b_WT
:
WhyType
b
}
,
forall
(
m
:
(
map
a
b
)),
forall
(
a1
:
a
)
(
a2
:
a
),
forall
(
b1
:
b
),
(
a1
=
a2
)
->
((
get
(
set
m
a1
b1
)
a2
)
=
b1
).
Axiom
Select_neq
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
{
b
:
Type
}
{
b_WT
:
WhyType
b
}
,
forall
(
m
:
(
map
a
b
)),
forall
(
a1
:
a
)
(
a2
:
a
),
forall
(
b1
:
b
),
(
~
(
a1
=
a2
))
->
((
get
(
set
m
a1
b1
)
a2
)
=
(
get
m
a2
)).
Parameter
const
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
{
b
:
Type
}
{
b_WT
:
WhyType
b
}
,
b
->
(
map
a
b
).
Axiom
Const
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
{
b
:
Type
}
{
b_WT
:
WhyType
b
}
,
forall
(
b1
:
b
)
(
a1
:
a
),
((
get
(
const
b1
:
(
map
a
b
))
a1
)
=
b1
).
(
*
Why3
assumption
*
)
Inductive
id
:=
|
Id
:
Z
->
id
.
Axiom
id_WhyType
:
WhyType
id
.
Existing
Instance
id_WhyType
.
(
*
Why3
assumption
*
)
Definition
state
:=
(
map
id
Z
).
(
*
Why3
assumption
*
)
Inductive
aexpr
:=
|
Anum
:
Z
->
aexpr
|
Avar
:
id
->
aexpr
|
Aadd
:
aexpr
->
aexpr
->
aexpr
|
Asub
:
aexpr
->
aexpr
->
aexpr
|
Amul
:
aexpr
->
aexpr
->
aexpr
.
Axiom
aexpr_WhyType
:
WhyType
aexpr
.
Existing
Instance
aexpr_WhyType
.
(
*
Why3
assumption
*
)
Inductive
bexpr
:=
|
Btrue
:
bexpr
|
Bfalse
:
bexpr
|
Band
:
bexpr
->
bexpr
->
bexpr
|
Bnot
:
bexpr
->
bexpr
|
Beq
:
aexpr
->
aexpr
->
bexpr
|
Ble
:
aexpr
->
aexpr
->
bexpr
.
Axiom
bexpr_WhyType
:
WhyType
bexpr
.
Existing
Instance
bexpr_WhyType
.
(
*
Why3
assumption
*
)
Inductive
com
:=
|
Cskip
:
com
|
Cassign
:
id
->
aexpr
->
com
|
Cseq
:
com
->
com
->
com
|
Cif
:
bexpr
->
com
->
com
->
com
|
Cwhile
:
bexpr
->
com
->
com
.
Axiom
com_WhyType
:
WhyType
com
.
Existing
Instance
com_WhyType
.
(
*
Why3
assumption
*
)
Fixpoint
aeval
(
st
:
(
map
id
Z
))
(
e
:
aexpr
)
{
struct
e
}:
Z
:=
match
e
with
|
(
Anum
n
)
=>
n
|
(
Avar
x
)
=>
(
get
st
x
)
|
(
Aadd
e1
e2
)
=>
((
aeval
st
e1
)
+
(
aeval
st
e2
))
%
Z
|
(
Asub
e1
e2
)
=>
((
aeval
st
e1
)
-
(
aeval
st
e2
))
%
Z
|
(
Amul
e1
e2
)
=>
((
aeval
st
e1
)
*
(
aeval
st
e2
))
%
Z
end
.
Parameter
beval
:
(
map
id
Z
)
->
bexpr
->
bool
.
Axiom
beval_def
:
forall
(
st
:
(
map
id
Z
))
(
b
:
bexpr
),
match
b
with
|
Btrue
=>
((
beval
st
b
)
=
true
)
|
Bfalse
=>
((
beval
st
b
)
=
false
)
|
(
Bnot
b
'
)
=>
((
beval
st
b
)
=
(
Init
.
Datatypes
.
negb
(
beval
st
b
'
)))
|
(
Band
b1
b2
)
=>
((
beval
st
b
)
=
(
Init
.
Datatypes
.
andb
(
beval
st
b1
)
(
beval
st
b2
)))
|
(
Beq
a1
a2
)
=>
(((
aeval
st
a1
)
=
(
aeval
st
a2
))
->
((
beval
st
b
)
=
true
))
/
\
((
~
((
aeval
st
a1
)
=
(
aeval
st
a2
)))
->
((
beval
st
b
)
=
false
))
|
(
Ble
a1
a2
)
=>
(((
aeval
st
a1
)
<=
(
aeval
st
a2
))
%
Z
->
((
beval
st
b
)
=
true
))
/
\
((
~
((
aeval
st
a1
)
<=
(
aeval
st
a2
))
%
Z
)
->
((
beval
st
b
)
=
false
))
end
.
Axiom
inversion_beval_t
:
forall
(
a1
:
aexpr
)
(
a2
:
aexpr
)
(
m
:
(
map
id
Z
)),
((
beval
m
(
Beq
a1
a2
))
=
true
)
->
((
aeval
m
a1
)
=
(
aeval
m
a2
)).
Axiom
inversion_beval_f
:
forall
(
a1
:
aexpr
)
(
a2
:
aexpr
)
(
m
:
(
map
id
Z
)),
((
beval
m
(
Beq
a1
a2
))
=
false
)
->
~
((
aeval
m
a1
)
=
(
aeval
m
a2
)).
(
*
Why3
assumption
*
)
Inductive
ceval
:
(
map
id
Z
)
->
com
->
(
map
id
Z
)
->
Prop
:=
|
E_Skip
:
forall
(
m
:
(
map
id
Z
)),
(
ceval
m
Cskip
m
)
|
E_Ass
:
forall
(
m
:
(
map
id
Z
))
(
a
:
aexpr
)
(
n
:
Z
)
(
x
:
id
),
((
aeval
m
a
)
=
n
)
->
(
ceval
m
(
Cassign
x
a
)
(
set
m
x
n
))
|
E_Seq
:
forall
(
cmd1
:
com
)
(
cmd2
:
com
)
(
m0
:
(
map
id
Z
))
(
m1
:
(
map
id
Z
))
(
m2
:
(
map
id
Z
)),
(
ceval
m0
cmd1
m1
)
->
((
ceval
m1
cmd2
m2
)
->
(
ceval
m0
(
Cseq
cmd1
cmd2
)
m2
))
|
E_IfTrue
:
forall
(
m0
:
(
map
id
Z
))
(
m1
:
(
map
id
Z
))
(
cond
:
bexpr
)
(
cmd1
:
com
)
(
cmd2
:
com
),
((
beval
m0
cond
)
=
true
)
->
((
ceval
m0
cmd1
m1
)
->
(
ceval
m0
(
Cif
cond
cmd1
cmd2
)
m1
))
|
E_IfFalse
:
forall
(
m0
:
(
map
id
Z
))
(
m1
:
(
map
id
Z
))
(
cond
:
bexpr
)
(
cmd1
:
com
)
(
cmd2
:
com
),
((
beval
m0
cond
)
=
false
)
->
((
ceval
m0
cmd2
m1
)
->
(
ceval
m0
(
Cif
cond
cmd1
cmd2
)
m1
))
|
E_WhileEnd
:
forall
(
cond
:
bexpr
)
(
m
:
(
map
id
Z
))
(
body
:
com
),
((
beval
m
cond
)
=
false
)
->
(
ceval
m
(
Cwhile
cond
body
)
m
)
|
E_WhileLoop
:
forall
(
mi
:
(
map
id
Z
))
(
mj
:
(
map
id
Z
))
(
mf
:
(
map
id
Z
))
(
cond
:
bexpr
)
(
body
:
com
),
((
beval
mi
cond
)
=
true
)
->
((
ceval
mi
body
mj
)
->
((
ceval
mj
(
Cwhile
cond
body
)
mf
)
->
(
ceval
mi
(
Cwhile
cond
body
)
mf
))).
Require
Import
Why3
.
Ltac
cvc
:=
why3
"CVC4,1.4,"
.
(
*
Why3
goal
*
)
Theorem
ceval_deterministic
:
forall
(
c
:
com
)
(
mi
:
(
map
id
Z
))
(
mf1
:
(
map
id
Z
))
(
mf2
:
(
map
id
Z
)),
(
ceval
mi
c
mf1
)
->
((
ceval
mi
c
mf2
)
->
(
mf1
=
mf2
)).
intros
c
mi
mf1
mf2
h1
h2
.
generalize
dependent
mf2
.
induction
h1
;
intros
mf2
h2
;
inversion
h2
;
cvc
.
Qed
.
examples/in_progress/mini-compiler/imp/why3session.xml
View file @
8a28f1b1
...
...
@@ -2,18 +2,191 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session
shape_version=
"4"
>
<prover
id=
"0"
name=
"C
oq
"
version=
"
8
.4
pl2
"
timelimit=
"5"
memlimit=
"1000"
/>
<prover
id=
"0"
name=
"C
VC4
"
version=
"
1
.4"
timelimit=
"5"
memlimit=
"1000"
/>
<prover
id=
"1"
name=
"Alt-Ergo"
version=
"0.95.2"
timelimit=
"5"
memlimit=
"1000"
/>
<file
name=
"../imp.why"
expanded=
"true"
>
<theory
name=
"Imp"
sum=
"939397712f6415b10da2ec9b4ffeab30"
expanded=
"true"
>
<goal
name=
"inversion_beval_t"
expanded=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.01"
/></proof>
</goal>
<goal
name=
"inversion_beval_f"
expanded=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.01"
/></proof>
<theory
name=
"Imp"
sum=
"8d9b512f0a2a1961484e5a0fa9ff9b68"
expanded=
"true"
>
<goal
name=
"ceval_deterministic_aux"
expanded=
"true"
>
<transf
name=
"induction_pr"
expanded=
"true"
>
<goal
name=
"ceval_deterministic_aux.1"
expl=
"1."
>
<transf
name=
"inversion_pr"
>
<goal
name=
"ceval_deterministic_aux.1.1"
expl=
"1."
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.01"
/></proof>
</goal>
<goal
name=
"ceval_deterministic_aux.1.2"
expl=
"2."
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.03"
/></proof>
</goal>
<goal
name=
"ceval_deterministic_aux.1.3"
expl=
"3."
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.02"
/></proof>
</goal>
<goal
name=
"ceval_deterministic_aux.1.4"
expl=
"4."
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.02"
/></proof>
</goal>
<goal
name=
"ceval_deterministic_aux.1.5"
expl=
"5."
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.02"
/></proof>
</goal>
<goal
name=
"ceval_deterministic_aux.1.6"
expl=
"6."
>