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
c56d7aaa
Commit
c56d7aaa
authored
Apr 11, 2011
by
Jean-Christophe Filliâtre
Browse files
Alt-ergo has no input syntax for triggers on existential quantifiers
parent
56135b10
Changes
3
Hide whitespace changes
Inline
Side-by-side
CHANGES
View file @
c56d7aaa
* marks an incompatible change
o fixed Alt-ergo output: no triggers for "exists" quantifier
o [IDE] tool "Replay" works
o [IDE] does not use Threads anymore, thanks to Call_provers.query_call
o VC gen produces explanations in a suitable form for IDE
...
...
examples/programs/tortoise_hare.mlw
0 → 100644
View file @
c56d7aaa
(* Floyd's ``the tortoise and the hare'' algorithm. *)
module TortoiseHare
use import int.Int
(* We consider a function f over an abstract type t *)
type t
logic f t : t
(* Given some x0 in t, we consider the sequence of the repeated calls
to f starting from x0. *)
logic x int : t
axiom xdef: forall n:int. n >= 0 -> x (n+1) = f (x n)
logic x0 : t = x 0
(* If t is finite, this sequence will eventually end up on a cycle.
Let us simply assume the existence of this cycle, that is
x (i + lambda) = x i, for some lambda > 0 and i large enough. *)
logic mu : int
axiom mu: mu >= 0
logic lambda : int
axiom lambda: lambda >= 1
axiom cycle: forall i:int. mu <= i -> x (i + lambda) = x i
lemma cycle_gen:
forall i:int. mu <= i -> forall k:int. 0 <= k -> x (i + lambda * k) = x i
(* The challenge is to prove that the recursive function
let rec run x1 x2 = if x1 <> x2 then run (f x1) (f (f x2))
terminates when called on x0 and (f x0).
*)
logic dist int int : int
axiom dist_def1:
forall n m: int. 0 <= n <= m ->
x (n + dist n m) = x m
axiom dist_def2:
forall n m: int. 0 <= n <= m ->
forall k: int. x (n + k) = x m -> dist n m <= k
logic r (x12 : (t, t)) (x'12 : (t, t)) =
let x1, x2 = x12 in
let x'1, x'2 = x'12 in
exists m:int.
x1 = x (m+1) and x2 = x (2*m+2) and x'1 = x m and x'2 = x (2*m) and
m < mu or (mu <= m and dist (m+1) (2*m+2) < dist m (2*m))
let rec run x1 x2 variant { (x1, x2) } with r =
{ exists m:int [x m]. x1 = x m and x2 = x (2*m) }
if x1 <> x2 then
run (f x1) (f (f x2))
{ }
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/tortoise_hare.gui"
End:
*)
src/printer/alt_ergo.ml
View file @
c56d7aaa
...
...
@@ -102,8 +102,11 @@ let rec print_fmla info fmt f = match f.f_node with
(
print_list
comma
(
print_term
info
))
tl
end
|
Fquant
(
q
,
fq
)
->
let
q
=
match
q
with
Fforall
->
"forall"
|
Fexists
->
"exists"
in
let
vl
,
tl
,
f
=
f_open_quant
fq
in
let
q
,
tl
=
match
q
with
|
Fforall
->
"forall"
,
tl
|
Fexists
->
"exists"
,
[]
(* Alt-ergo has no triggers for exists *)
in
let
forall
fmt
v
=
fprintf
fmt
"%s %a:%a"
q
print_ident
v
.
vs_name
(
print_type
info
)
v
.
vs_ty
in
...
...
@@ -141,8 +144,7 @@ and print_triggers info fmt tl =
|
Term
_
->
true
|
Fmla
{
f_node
=
Fapp
(
ps
,_
)}
->
not
(
ls_equal
ps
ps_equ
)
|
_
->
false
in
let
tl
=
List
.
map
(
List
.
filter
filter
)
tl
in
let
tl
=
List
.
map
(
List
.
filter
filter
)
tl
in
let
tl
=
List
.
filter
(
function
[]
->
false
|
_
::_
->
true
)
tl
in
if
tl
=
[]
then
()
else
fprintf
fmt
"@ [%a]"
(
print_list
alt
(
print_list
comma
(
print_expr
info
)))
tl
...
...
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