Commit e602b246 authored by Francois Bobot's avatar Francois Bobot
Browse files

Example provenant du harness de heap sort de vacid

parent b78caa70
theory Sorted
use import int.Int
use real.Real
use import array.Array
type array = (int, real) t
type multi = (real, int) t
logic n : int = 4
logic sorted(m : array) =
forall x,y:int. x<=y -> Real.(<=)(select(m, x),select(m, y))
logic count(m : array, i : int, j : int, v : real) : int =
if i = j then 0 else
let c = count(m,i+1,j,v) in
(if select (m,i) = v then c + 1 else c)
logic model(m1 : array, m2 : multi) =
forall v:real. count(m1,1,n+1,v) = select(m2,v)
(*
logic model_aux(m1 : array, i : int) : multi
axiom Model_aux_def1 :
forall m1 : array. forall i : int. forall v : real.
1 <= i and i <= n ->
select(model_aux(m1,i),v) =
if select(m1,i)=v then select(model_aux(m1,i+1),v) + 1
else select(model_aux(m1,i+1),v)
axiom Model_aux_def2 :
forall m1 : array. forall v : real. select(model_aux(m1,n+1),v) = 0
logic model(m1 : array, m2 : multi) = model_aux(m1, 1) = m2
*)
(*axiom TPTP : 1 < 2 and 2 < 3 and 3 < 4 and 13 < 42 and
0+1 = 1 and 1+1 = 2 and 2+1 = 3 and 3+1 = 4
axiom TPTP2 : forall x,y : real. x < y -> x<>y*)
goal G :
forall m1 : array.
select(m1,1) = 42. ->
select(m1,2) = 13. ->
select(m1,3) = 42. ->
select(m1,4) = 45. ->
forall m2 : array.
forall multi : multi.
model(m1,multi) ->
model(m2,multi) ->
sorted(m2) ->
select(m2,1) = 13. and
select(m2,2) = 42. and
select(m2,3) = 42. and
select(m2,4) = 45.
(* goal G_false :
forall m1 : array.
select(m1,1) = 42. ->
select(m1,2) = 13. ->
select(m1,3) = 42. ->
forall m2 : array.
forall multi : multi.
model(m1,multi) ->
model(m2,multi) ->
sorted(m2) ->
select(m2,1) = 42. and
select(m2,2) = 13. and
select(m2,3) = 42.
*)
end
\ No newline at end of file
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment