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
6b0eda19
Commit
6b0eda19
authored
Oct 18, 2012
by
MARCHE Claude
Browse files
a few tests
parent
7845b21e
Changes
4
Hide whitespace changes
Inline
Side-by-side
tests/test-ind.why
0 → 100644
View file @
6b0eda19
theory T
type list 'a = Nil | Cons 'a (list 'a)
function app (l1:list 'a) (l2:list 'a) : (list 'a) =
match l1 with
| Nil -> l2
| Cons x r -> Cons x (app r l2)
end
lemma app_nil : forall l:list 'a. app l Nil = l
type tree = Leaf int | Node tree tree
end
tests/test-ind/why3session.xml
0 → 100644
View file @
6b0eda19
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
<why3session
name=
"test-ind/why3session.xml"
shape_version=
"2"
>
<file
name=
"../test-ind.why"
verified=
"false"
expanded=
"true"
>
<theory
name=
"T"
locfile=
"test-ind/../test-ind.why"
loclnum=
"2"
loccnumb=
"7"
loccnume=
"8"
verified=
"false"
expanded=
"true"
>
<goal
name=
"app_nil"
locfile=
"test-ind/../test-ind.why"
loclnum=
"12"
loccnumb=
"6"
loccnume=
"13"
sum=
"57a6eece27d97fc131ecc13471649486"
proved=
"false"
expanded=
"true"
shape=
"ainfix =aappV0aNilV0F"
>
</goal>
</theory>
</file>
</why3session>
tests/test-settheory.why
0 → 100644
View file @
6b0eda19
theory TestOverriding
use import settheory.Relation
use import settheory.InverseDomRan
use import settheory.Overriding
use import settheory.Function
constant f : rel int int = singleton (3,4)
constant g : rel int int = f <+ (singleton (5,6))
constant h : rel int int = g <+ (singleton (3,7))
goal testdom1: mem 3 (dom g)
goal testdom2: mem 3 (dom h)
goal testapply1: apply f 3 = 4
goal testapply2: apply g 3 = 4
goal testapply3: apply g 5 = 6
goal testapply4: apply h 3 = 7
goal testapply5: apply h 5 = 6
goal testapply_smoke1: apply h 3 = 8
goal testapply_smoke2: apply h 5 = 9
end
theory TestCompose
use import settheory.Relation
use import settheory.InverseDomRan
use import settheory.Composition
use import settheory.Function
constant f : rel int int = singleton (3,4)
constant g : rel int int = singleton (4,6)
constant h : rel int int = semicolon f g
use import settheory.Interval
constant fun_int_int : set (rel int int) = integer +-> integer
(*
lemma f_is_fun : mem f fun_int_int
lemma g_is_fun : mem g fun_int_int
lemma h_is_fun : mem h fun_int_int
*)
goal test1: mem (apply h 3) (Interval.mk 0 10)
goal test2: 0 <= apply h 3 <= 10
goal test3: apply h 3 = 6
end
tests/test-settheory/why3session.xml
0 → 100644
View file @
6b0eda19
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/cmarche/recherche/why3/share/why3session.dtd">
<why3session
shape_version=
"2"
>
<prover
id=
"0"
name=
"Alt-Ergo"
version=
"0.94"
/>
<prover
id=
"1"
name=
"Alt-Ergo"
version=
"0.95-dev"
/>
<prover
id=
"2"
name=
"CVC3"
version=
"2.2"
/>
<prover
id=
"3"
name=
"CVC3"
version=
"2.4.1"
/>
<prover
id=
"4"
name=
"Z3"
version=
"2.19"
/>
<prover
id=
"5"
name=
"Z3"
version=
"3.2"
/>
<prover
id=
"6"
name=
"Z3"
version=
"4.0"
/>
<file
name=
"../test-settheory.why"
verified=
"false"
expanded=
"true"
>
<theory
name=
"TestOverriding"
locfile=
"../test-settheory.why"
loclnum=
"2"
loccnumb=
"7"
loccnume=
"21"
verified=
"false"
expanded=
"false"
>
<goal
name=
"testdom1"
locfile=
"../test-settheory.why"
loclnum=
"13"
loccnumb=
"7"
loccnume=
"15"
sum=
"8a0b40d245bb0d25f0dbb133e52eae35"
proved=
"false"
expanded=
"false"
shape=
"amemc3adomag"
>
<proof
prover=
"0"
timelimit=
"5"
memlimit=
"1000"
obsolete=
"true"
archived=
"false"
>
<result
status=
"valid"
time=
"0.03"
/>
</proof>
<proof
prover=
"2"
timelimit=
"5"
memlimit=
"1000"
obsolete=
"true"
archived=
"false"
>
<result
status=
"valid"
time=
"4.09"
/>
</proof>
<proof
prover=
"5"
timelimit=
"5"
memlimit=
"1000"
obsolete=
"true"
archived=
"false"
>
<result
status=
"valid"
time=
"0.09"
/>
</proof>
<proof
prover=
"6"
timelimit=
"5"
memlimit=
"1000"
obsolete=
"true"
archived=
"false"
>
<result
status=
"valid"
time=
"0.12"
/>
</proof>
</goal>
<goal
name=
"testdom2"
locfile=
"../test-settheory.why"
loclnum=
"14"
loccnumb=
"7"
loccnume=
"15"
sum=
"8f2ab43f6ffef60ad28fb26bcb6351b6"
proved=
"false"
expanded=
"false"
shape=
"amemc3adomah"
>
<proof
prover=
"0"
timelimit=
"5"
memlimit=
"1000"
obsolete=
"true"
archived=
"false"
>
<result
status=
"valid"
time=
"0.10"
/>
</proof>
<proof
prover=
"2"
timelimit=
"5"
memlimit=
"1000"
obsolete=
"true"
archived=
"false"
>
<result
status=
"valid"
time=
"0.66"
/>
</proof>
<proof
prover=
"3"
timelimit=
"5"
memlimit=
"1000"
obsolete=
"true"
archived=
"false"
>
<result
status=
"valid"
time=
"1.17"
/>
</proof>
<proof
prover=
"5"
timelimit=
"5"
memlimit=
"1000"
obsolete=
"true"
archived=
"false"
>
<result
status=
"valid"
time=
"0.10"
/>
</proof>
<proof
prover=
"6"
timelimit=
"5"
memlimit=
"1000"
obsolete=
"true"
archived=
"false"
>
<result
status=
"valid"
time=
"0.15"
/>
</proof>
</goal>
<goal
name=
"testapply1"
locfile=
"../test-settheory.why"
loclnum=
"16"
loccnumb=
"7"
loccnume=
"17"
sum=
"4b0a5282797ea125bc2496d455749ace"
proved=
"false"
expanded=
"false"
shape=
"ainfix =aapplyafc3c4"
>
<proof
prover=
"0"
timelimit=
"5"
memlimit=
"1000"
obsolete=
"true"
archived=
"false"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
<proof
prover=
"2"
timelimit=
"5"
memlimit=
"1000"
obsolete=
"true"
archived=
"false"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
<proof
prover=
"3"
timelimit=
"5"
memlimit=
"1000"
obsolete=
"true"
archived=
"false"
>
<result
status=
"valid"
time=
"0.03"
/>
</proof>
<proof
prover=
"5"
timelimit=
"5"
memlimit=
"1000"
obsolete=
"true"
archived=
"false"
>
<result
status=
"valid"
time=
"0.07"
/>
</proof>
<proof
prover=
"6"
timelimit=
"5"
memlimit=
"1000"
obsolete=
"true"
archived=
"false"
>
<result
status=
"valid"
time=
"0.08"
/>
</proof>
</goal>
<goal
name=
"testapply2"
locfile=
"../test-settheory.why"
loclnum=
"18"
loccnumb=
"7"
loccnume=
"17"
sum=
"8f6f1c570e478e86e60b9e7a6714b05e"
proved=
"false"
expanded=
"false"
shape=
"ainfix =aapplyagc3c4"
>
<proof
prover=
"2"
timelimit=
"5"
memlimit=
"1000"
obsolete=
"true"
archived=
"false"
>
<result
status=
"valid"
time=
"0.04"
/>
</proof>
<proof
prover=
"3"
timelimit=
"5"
memlimit=
"1000"
obsolete=
"true"
archived=
"false"
>
<result
status=
"valid"
time=
"0.04"
/>
</proof>
<proof
prover=
"5"
timelimit=
"5"
memlimit=
"1000"
obsolete=
"true"
archived=
"false"
>
<result
status=
"valid"
time=
"0.07"
/>
</proof>
<proof
prover=
"6"
timelimit=
"5"
memlimit=
"1000"
obsolete=
"true"
archived=
"false"
>
<result
status=
"valid"
time=
"0.09"
/>
</proof>
</goal>
<goal
name=
"testapply3"
locfile=
"../test-settheory.why"
loclnum=
"19"
loccnumb=
"7"
loccnume=
"17"
sum=
"1f4a81dfde1d341b653d75525b2dd53e"
proved=
"false"
expanded=
"false"
shape=
"ainfix =aapplyagc5c6"
>
<proof
prover=
"0"
timelimit=
"5"
memlimit=
"1000"
obsolete=
"true"
archived=
"false"
>
<result
status=
"valid"
time=
"0.04"
/>
</proof>
<proof
prover=
"2"
timelimit=
"5"
memlimit=
"1000"
obsolete=
"true"
archived=
"false"
>
<result
status=
"valid"
time=
"0.23"
/>
</proof>
<proof
prover=
"3"
timelimit=
"5"
memlimit=
"1000"
obsolete=
"true"
archived=
"false"
>
<result
status=
"valid"
time=
"0.31"
/>
</proof>
<proof
prover=
"5"
timelimit=
"5"
memlimit=
"1000"
obsolete=
"true"
archived=
"false"
>
<result
status=
"valid"
time=
"0.06"
/>
</proof>
<proof
prover=
"6"
timelimit=
"5"
memlimit=
"1000"
obsolete=
"true"
archived=
"false"
>
<result
status=
"valid"
time=
"0.08"
/>
</proof>
</goal>
<goal
name=
"testapply4"
locfile=
"../test-settheory.why"
loclnum=
"21"
loccnumb=
"7"
loccnume=
"17"
sum=
"2ee96d72dd795975902796738d05f4c1"
proved=
"false"
expanded=
"false"
shape=
"ainfix =aapplyahc3c7"
>
<proof
prover=
"0"
timelimit=
"5"
memlimit=
"1000"
obsolete=
"true"
archived=
"false"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
<proof
prover=
"2"
timelimit=
"5"
memlimit=
"1000"
obsolete=
"true"
archived=
"false"
>
<result
status=
"valid"
time=
"0.39"
/>
</proof>
<proof
prover=
"3"
timelimit=
"5"
memlimit=
"1000"
obsolete=
"true"
archived=
"false"
>
<result
status=
"valid"
time=
"0.56"
/>
</proof>
<proof
prover=
"5"
timelimit=
"5"
memlimit=
"1000"
obsolete=
"true"
archived=
"false"
>
<result
status=
"valid"
time=
"0.06"
/>
</proof>
<proof
prover=
"6"
timelimit=
"5"
memlimit=
"1000"
obsolete=
"true"
archived=
"false"
>
<result
status=
"valid"
time=
"0.08"
/>
</proof>
</goal>
<goal
name=
"testapply5"
locfile=
"../test-settheory.why"
loclnum=
"22"
loccnumb=
"7"
loccnume=
"17"
sum=
"e3e0b139fb84a8dab3a45c0cada174aa"
proved=
"false"
expanded=
"false"
shape=
"ainfix =aapplyahc5c6"
>
<proof
prover=
"3"
timelimit=
"5"
memlimit=
"1000"
obsolete=
"true"
archived=
"false"
>
<result
status=
"valid"
time=
"4.49"
/>
</proof>
<proof
prover=
"5"
timelimit=
"5"
memlimit=
"1000"
obsolete=
"true"
archived=
"false"
>
<result
status=
"valid"
time=
"0.20"
/>
</proof>
<proof
prover=
"6"
timelimit=
"5"
memlimit=
"1000"
obsolete=
"true"
archived=
"false"
>
<result
status=
"valid"
time=
"2.72"
/>
</proof>
</goal>
<goal
name=
"testapply_smoke1"
locfile=
"../test-settheory.why"
loclnum=
"24"
loccnumb=
"7"
loccnume=
"23"
sum=
"899b7dfb6506e58cc6134b0f306e2a79"
proved=
"false"
expanded=
"false"
shape=
"ainfix =aapplyahc3c8"
>
<proof
prover=
"0"
timelimit=
"5"
memlimit=
"1000"
obsolete=
"true"
archived=
"false"
>
<result
status=
"unknown"
time=
"0.15"
/>
</proof>
<proof
prover=
"2"
timelimit=
"5"
memlimit=
"1000"
obsolete=
"true"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.04"
/>
</proof>
<proof
prover=
"3"
timelimit=
"5"
memlimit=
"1000"
obsolete=
"true"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.03"
/>
</proof>
<proof
prover=
"5"
timelimit=
"5"
memlimit=
"1000"
obsolete=
"true"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.04"
/>
</proof>
<proof
prover=
"6"
timelimit=
"5"
memlimit=
"1000"
obsolete=
"true"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.07"
/>
</proof>
</goal>
<goal
name=
"testapply_smoke2"
locfile=
"../test-settheory.why"
loclnum=
"25"
loccnumb=
"7"
loccnume=
"23"
sum=
"1167af1a895bbeb62d93e3070b18169c"
proved=
"false"
expanded=
"false"
shape=
"ainfix =aapplyahc5c9"
>
<proof
prover=
"0"
timelimit=
"5"
memlimit=
"1000"
obsolete=
"true"
archived=
"false"
>
<result
status=
"unknown"
time=
"0.16"
/>
</proof>
<proof
prover=
"2"
timelimit=
"5"
memlimit=
"1000"
obsolete=
"true"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.04"
/>
</proof>
<proof
prover=
"3"
timelimit=
"5"
memlimit=
"1000"
obsolete=
"true"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.14"
/>
</proof>
<proof
prover=
"5"
timelimit=
"5"
memlimit=
"1000"
obsolete=
"true"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.24"
/>
</proof>
<proof
prover=
"6"
timelimit=
"5"
memlimit=
"1000"
obsolete=
"true"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.38"
/>
</proof>
</goal>
</theory>
<theory
name=
"TestCompose"
locfile=
"../test-settheory.why"
loclnum=
"29"
loccnumb=
"7"
loccnume=
"18"
verified=
"false"
expanded=
"true"
>
<goal
name=
"test1"
locfile=
"../test-settheory.why"
loclnum=
"52"
loccnumb=
"7"
loccnume=
"12"
sum=
"e76b4442af5b67d8532e86f8c6cbb5a1"
proved=
"false"
expanded=
"true"
shape=
"amemaapplyahc3amkc0c10"
>
<proof
prover=
"0"
timelimit=
"5"
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"unknown"
time=
"0.03"
/>
</proof>
<proof
prover=
"1"
timelimit=
"3"
memlimit=
"1000"
edited=
"testmnsettheory-TestCompose-test1_1.why"
obsolete=
"false"
archived=
"false"
>
<result
status=
"highfailure"
time=
"0.10"
/>
</proof>
<proof
prover=
"2"
timelimit=
"5"
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.11"
/>
</proof>
<proof
prover=
"3"
timelimit=
"5"
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.51"
/>
</proof>
<proof
prover=
"4"
timelimit=
"5"
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.06"
/>
</proof>
<proof
prover=
"5"
timelimit=
"5"
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.14"
/>
</proof>
<proof
prover=
"6"
timelimit=
"5"
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.14"
/>
</proof>
</goal>
<goal
name=
"test2"
locfile=
"../test-settheory.why"
loclnum=
"54"
loccnumb=
"7"
loccnume=
"12"
sum=
"5c53ae5d94cefefac7135845b5506946"