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
314bc03f
Commit
314bc03f
authored
Mar 26, 2010
by
Jean-Christophe Filliâtre
Browse files
syntaxe a <= b <= c (pour des operateurs quelconques, bien entendu)
parent
bac4d8d1
Changes
6
Hide whitespace changes
Inline
Side-by-side
examples/programs/bresenham.mlw
View file @
314bc03f
...
...
@@ -12,7 +12,7 @@
{
logic x2 : int
logic y2 : int
axiom First_octant : 0 <= y2
and y2
<= x2
axiom First_octant : 0 <= y2 <= x2
}
(* The code.
...
...
@@ -29,7 +29,7 @@ logic best(x:int, y:int) =
logic invariant(x:int, y:int, e:int) =
e = 2 * (x + 1) * y2 - (2 * y + 1) * x2 and
2 * (y2 - x2) <= e
and e
<= 2 * y2
2 * (y2 - x2) <= e <= 2 * y2
lemma Invariant_is_ok : forall x,y,e:int. invariant(x,y,e) -> best(x,y)
}
...
...
src/parser/parser.mly
View file @
314bc03f
...
...
@@ -32,10 +32,10 @@
let
mk_pat
p
=
{
pat_loc
=
loc
()
;
pat_desc
=
p
}
let
infix_ppl
loc
a
i
b
=
mk_ppl
loc
(
PPin
fix
(
a
,
i
,
b
))
let
infix_ppl
loc
a
i
b
=
mk_ppl
loc
(
PP
b
in
op
(
a
,
i
,
b
))
let
infix_pp
a
i
b
=
infix_ppl
(
loc
()
)
a
i
b
let
prefix_ppl
loc
p
a
=
mk_ppl
loc
(
PP
prefix
(
p
,
a
))
let
prefix_ppl
loc
p
a
=
mk_ppl
loc
(
PP
unop
(
p
,
a
))
let
prefix_pp
p
a
=
prefix_ppl
(
loc
()
)
p
a
let
infix
s
=
"infix "
^
s
...
...
@@ -359,19 +359,19 @@ lexpr:
{
prefix_pp
PPnot
$
2
}
|
lexpr
EQUAL
lexpr
{
let
id
=
{
id
=
infix
"="
;
id_loc
=
loc_i
2
}
in
mk_pp
(
PP
app
(
Qident
id
,
[
$
1
;
$
3
]
))
}
mk_pp
(
PP
infix
(
$
1
,
id
,
$
3
))
}
|
lexpr
OP1
lexpr
{
let
id
=
{
id
=
infix
$
2
;
id_loc
=
loc_i
2
}
in
mk_pp
(
PP
app
(
Qident
id
,
[
$
1
;
$
3
]
))
}
mk_pp
(
PP
infix
(
$
1
,
id
,
$
3
))
}
|
lexpr
OP2
lexpr
{
let
id
=
{
id
=
infix
$
2
;
id_loc
=
loc_i
2
}
in
mk_pp
(
PP
app
(
Qident
id
,
[
$
1
;
$
3
]
))
}
mk_pp
(
PP
infix
(
$
1
,
id
,
$
3
))
}
|
lexpr
OP3
lexpr
{
let
id
=
{
id
=
infix
$
2
;
id_loc
=
loc_i
2
}
in
mk_pp
(
PP
app
(
Qident
id
,
[
$
1
;
$
3
]
))
}
mk_pp
(
PP
infix
(
$
1
,
id
,
$
3
))
}
|
lexpr
OP4
lexpr
{
let
id
=
{
id
=
infix
$
2
;
id_loc
=
loc_i
2
}
in
mk_pp
(
PP
app
(
Qident
id
,
[
$
1
;
$
3
]
))
}
mk_pp
(
PP
infix
(
$
1
,
id
,
$
3
))
}
|
any_op
lexpr
%
prec
prefix_op
{
let
id
=
{
id
=
prefix
$
1
;
id_loc
=
loc_i
2
}
in
mk_pp
(
PPapp
(
Qident
id
,
[
$
2
]))
}
...
...
src/parser/ptree.mli
View file @
314bc03f
...
...
@@ -29,10 +29,10 @@ type constant = Term.constant
type
pp_quant
=
|
PPforall
|
PPexists
type
pp_in
fix
=
type
pp_
b
in
op
=
|
PPand
|
PPor
|
PPimplies
|
PPiff
type
pp_
prefix
=
type
pp_
unop
=
|
PPnot
type
ident
=
{
id
:
string
;
id_loc
:
loc
}
...
...
@@ -66,8 +66,9 @@ and pp_desc =
|
PPtrue
|
PPfalse
|
PPconst
of
constant
|
PPinfix
of
lexpr
*
pp_infix
*
lexpr
|
PPprefix
of
pp_prefix
*
lexpr
|
PPinfix
of
lexpr
*
ident
*
lexpr
|
PPbinop
of
lexpr
*
pp_binop
*
lexpr
|
PPunop
of
pp_unop
*
lexpr
|
PPif
of
lexpr
*
lexpr
*
lexpr
|
PPquant
of
pp_quant
*
uquant
list
*
lexpr
list
list
*
lexpr
|
PPnamed
of
string
*
lexpr
...
...
src/parser/typing.ml
View file @
314bc03f
...
...
@@ -220,18 +220,20 @@ let specialize_lsymbol p uc =
s
,
specialize_lsymbol
(
qloc
p
)
s
let
specialize_fsymbol
p
uc
=
let
loc
=
qloc
p
in
let
s
,
(
tl
,
ty
)
=
specialize_lsymbol
p
uc
in
match
ty
with
|
None
->
error
~
loc
TermExpected
|
None
->
let
loc
=
qloc
p
in
error
~
loc
TermExpected
|
Some
ty
->
s
,
tl
,
ty
let
specialize_psymbol
p
uc
=
let
loc
=
qloc
p
in
let
s
,
(
tl
,
ty
)
=
specialize_lsymbol
p
uc
in
match
ty
with
|
None
->
s
,
tl
|
Some
_
->
error
~
loc
PredicateExpected
|
Some
_
->
let
loc
=
qloc
p
in
error
~
loc
PredicateExpected
let
is_psymbol
p
uc
=
let
s
=
find_lsymbol
p
uc
in
s
.
ls_value
=
None
(** Typing types *)
...
...
@@ -373,6 +375,10 @@ and dterm_node loc env = function
let
s
,
tyl
,
ty
=
specialize_fsymbol
x
env
.
uc
in
let
tl
=
dtype_args
s
.
ls_name
loc
env
tyl
tl
in
Tapp
(
s
,
tl
)
,
ty
|
PPinfix
(
e1
,
x
,
e2
)
->
let
s
,
tyl
,
ty
=
specialize_fsymbol
(
Qident
x
)
env
.
uc
in
let
tl
=
dtype_args
s
.
ls_name
loc
env
tyl
[
e1
;
e2
]
in
Tapp
(
s
,
tl
)
,
ty
|
PPconst
(
ConstInt
_
as
c
)
->
Tconst
c
,
Tyapp
(
Ty
.
ts_int
,
[]
)
|
PPconst
(
ConstReal
_
as
c
)
->
...
...
@@ -414,7 +420,7 @@ and dterm_node loc env = function
let
e1
=
dfmla
env
e1
in
Teps
(
x
,
ty
,
e1
)
,
ty
|
PPquant
_
|
PPif
_
|
PP
prefix
_
|
PP
infix
_
|
PPfalse
|
PPtrue
->
|
PP
binop
_
|
PP
unop
_
|
PPfalse
|
PPtrue
->
error
~
loc
TermExpected
and
dfmla
env
e
=
match
e
.
pp_desc
with
...
...
@@ -422,9 +428,9 @@ and dfmla env e = match e.pp_desc with
Ftrue
|
PPfalse
->
Ffalse
|
PP
prefix
(
PPnot
,
a
)
->
|
PP
unop
(
PPnot
,
a
)
->
Fnot
(
dfmla
env
a
)
|
PPin
fix
(
a
,
(
PPand
|
PPor
|
PPimplies
|
PPiff
as
op
)
,
b
)
->
|
PP
b
in
op
(
a
,
(
PPand
|
PPor
|
PPimplies
|
PPiff
as
op
)
,
b
)
->
Fbinop
(
binop
op
,
dfmla
env
a
,
dfmla
env
b
)
|
PPif
(
a
,
b
,
c
)
->
Fif
(
dfmla
env
a
,
dfmla
env
b
,
dfmla
env
c
)
...
...
@@ -456,6 +462,16 @@ and dfmla env e = match e.pp_desc with
let
s
,
tyl
=
specialize_psymbol
x
env
.
uc
in
let
tl
=
dtype_args
s
.
ls_name
e
.
pp_loc
env
tyl
tl
in
Fapp
(
s
,
tl
)
|
PPinfix
(
e12
,
op2
,
e3
)
->
begin
match
e12
.
pp_desc
with
|
PPinfix
(
_
,
op1
,
e2
)
when
is_psymbol
(
Qident
op1
)
env
.
uc
->
let
e23
=
{
e
with
pp_desc
=
PPinfix
(
e2
,
op2
,
e3
)
}
in
Fbinop
(
Fand
,
dfmla
env
e12
,
dfmla
env
e23
)
|
_
->
let
s
,
tyl
=
specialize_psymbol
(
Qident
op2
)
env
.
uc
in
let
tl
=
dtype_args
s
.
ls_name
e
.
pp_loc
env
tyl
[
e12
;
e3
]
in
Fapp
(
s
,
tl
)
end
|
PPlet
({
id
=
x
}
,
e1
,
e2
)
->
let
e1
=
dterm
env
e1
in
let
ty
=
e1
.
dt_ty
in
...
...
theories/int.why
View file @
314bc03f
...
...
@@ -56,7 +56,7 @@ theory EuclideanDivision
forall x,y:int. y <> 0 -> x = y * div(x,y) + mod(x,y)
axiom Mod_bound:
forall x,y:int. y <> 0 -> 0 <= mod(x,y)
and mod(x,y)
< abs(y)
forall x,y:int. y <> 0 -> 0 <= mod(x,y) < abs(y)
lemma Mod_1: forall x:int. mod(x,1) = 0
...
...
@@ -76,7 +76,7 @@ theory ComputerDivision
forall x,y:int. y <> 0 -> x = y * div(x,y) + mod(x,y)
axiom Mod_bound:
forall x,y:int. y <> 0 -> -abs(y) < mod(x,y)
and mod(x,y)
< abs(y)
forall x,y:int. y <> 0 -> -abs(y) < mod(x,y) < abs(y)
lemma Mod_1: forall x:int. mod(x,1) = 0
...
...
theories/real.why
View file @
314bc03f
...
...
@@ -25,7 +25,7 @@ theory Abs
axiom Pos: forall x:real. x >= 0.0 -> abs(x) = x
axiom Neg: forall x:real. x <= 0.0 -> abs(x) = -x
lemma Abs_le: forall x,y:real. abs(x) <= y <-> -y <= x
and x
<= y
lemma Abs_le: forall x,y:real. abs(x) <= y <-> -y <= x <= y
lemma Abs_pos: forall x:real. abs(x) >= 0.0
...
...
@@ -221,7 +221,7 @@ theory Hyperbolic
forall x:real. x >= 1.0 -> arcosh(x) = log(x+sqrt(sqr(x)-1.0))
logic artanh(x:real) : real
axiom Artanh_def:
forall x:real. -1.0 < x
and x
< 1.0 -> artanh(x) = 0.5*log((1.0+x)/(1.0-x))
forall x:real. -1.0 < x < 1.0 -> artanh(x) = 0.5*log((1.0+x)/(1.0-x))
end
...
...
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