Commit 5a01c422 authored by MARCHE Claude's avatar MARCHE Claude

Theory of sets: split/clone between finite and infinite sets

parent 27538456
......@@ -4,6 +4,10 @@
== Papers to write ==
* paper on the module system, its semantics, realizations, avec en
particulier la solution avec les types classes qui reste a
implanter
* DONE Encodings and transformations (Andrei+Francois)
* DONE Why presentation at the IVL workshop of CADE:
(http://research.microsoft.com/en-us/um/people/moskal/boogie2011/)
......@@ -101,14 +105,17 @@
* Coq tactic
** ajout de bases de hint
* Coq output
* PRIORITAIRE Coq output
- corriger l'incoherence, comprendre si on veut vraiment accepter
function x : 'a
(cf: en caml cela ne marche pas)
Solution proposee: utiliser des types classes, en particulier Inhabited
* new language constructs
** sandbox, abstract
** NOT NEEDED ANYMORE sandbox
** DONE abstract e { q }
** contract e { q }
* efficiency issues
- understand problems when large number of goals (cf D Mentré examples)
......@@ -202,7 +209,7 @@ See manual Section xx
== TODOs ==
* BUG CVC3 avec la division par 0, cf examples/tests-provers/cvc3.why
* DONE bug CVC3 avec la division par 0, cf examples/tests-provers/cvc3.why
* DONE Document the Coq plugin and tactic
** DONE option timelimit <n>
......
theory Th1
use import set.Fsetint
(* proved with vampire 0.6 and eprover 1.4 *)
lemma l_false : false
end
theory Th2
use import set.Fsetint
function integer : set int
lemma mem_integer: forall x:int. mem x integer
goal foo : false
end
theory Th3
use import int.Int
type set 'a
function f (set int) : int
function g (set int) : int
axiom axiom1: forall s: set int, x: int. f s <= x <= g s
goal foo : false
end
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
<why3session
name="fsetint/why3session.xml">
<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"/>
<file
name="../fsetint.why"
verified="false"
expanded="true">
<theory
name="Th1"
locfile="fsetint/../fsetint.why"
loclnum="2" loccnumb="7" loccnume="10"
verified="false"
expanded="true">
<goal
name="l_false"
locfile="fsetint/../fsetint.why"
loclnum="5" loccnumb="9" loccnume="16"
sum="dccc55c14590d1b87dbed47d9b0b7ca4"
proved="false"
expanded="true"
shape="f">
<proof
prover="4"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="3.42"/>
</proof>
<proof
prover="2"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="3.23"/>
</proof>
<proof
prover="0"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.02"/>
</proof>
<proof
prover="3"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="3.65"/>
</proof>
<proof
prover="5"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="3.53"/>
</proof>
<proof
prover="1"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.03"/>
</proof>
</goal>
</theory>
<theory
name="Th2"
locfile="fsetint/../fsetint.why"
loclnum="9" loccnumb="7" loccnume="10"
verified="false"
expanded="true">
<goal
name="mem_integer"
locfile="fsetint/../fsetint.why"
loclnum="13" loccnumb="8" loccnume="19"
sum="83012d44889c35b4b77dfddaf6119875"
proved="false"
expanded="true"
shape="amemV0aintegerF">
<proof
prover="4"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="3.22"/>
</proof>
<proof
prover="2"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="3.13"/>
</proof>
<proof
prover="0"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.01"/>
</proof>
<proof
prover="3"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="3.22"/>
</proof>
<proof
prover="5"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="3.22"/>
</proof>
<proof
prover="1"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.02"/>
</proof>
</goal>
<goal
name="foo"
locfile="fsetint/../fsetint.why"
loclnum="15" loccnumb="7" loccnume="10"
sum="1ac5f7ac42f0e2a8b0d1a1f11f9f0d71"
proved="false"
expanded="true"
shape="f">
<proof
prover="4"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="3.13"/>
</proof>
<proof
prover="2"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="3.04"/>
</proof>
<proof
prover="0"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.01"/>
</proof>
<proof
prover="3"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="3.32"/>
</proof>
<proof
prover="5"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="3.12"/>
</proof>
<proof
prover="1"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.02"/>
</proof>
</goal>
</theory>
<theory
name="Th3"
locfile="fsetint/../fsetint.why"
loclnum="20" loccnumb="7" loccnume="10"
verified="false"
expanded="true">
<goal
name="foo"
locfile="fsetint/../fsetint.why"
loclnum="30" loccnumb="7" loccnume="10"
sum="298aff6b85501a01c5fd7cab28f641d0"
proved="false"
expanded="true"
shape="f">
<proof
prover="4"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.02"/>
</proof>
<proof
prover="2"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
</proof>
<proof
prover="0"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.01"/>
</proof>
<proof
prover="3"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
</proof>
<proof
prover="5"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.02"/>
</proof>
<proof
prover="1"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.02"/>
</proof>
</goal>
</theory>
</file>
</why3session>
This diff is collapsed.
......@@ -3,7 +3,7 @@
(** {2 General Sets} *)
theory Set
theory SetGen
type set 'a
......@@ -78,12 +78,19 @@ theory Set
axiom choose_def:
forall s: set 'a. not (is_empty s) -> mem (choose s) s
(*
end
(** {2 Potentially infinite sets} *)
theory Set
clone export SetGen
(** the set of all x of type 'a *)
constant all: set 'a
axiom all_def: forall x: 'a. mem x all
*)
end
(** {2 Set Comprehension} *)
......@@ -119,7 +126,7 @@ end
theory Fset
use import int.Int
clone export Set
clone export SetGen
function cardinal (set 'a) : int
......@@ -206,17 +213,6 @@ theory Fsetint
end
(** {2 Set extensionality} *)
theory FsetExt
use export Fset
axiom ext: forall s1 s2 : set 'a.
s1 = s2 <-> (forall x : 'a. mem x s1 <-> mem x s2)
end
(** {2 Sets realized as maps} *)
theory SetMap
......
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