Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
why3
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
113
Issues
113
List
Boards
Labels
Service Desk
Milestones
Merge Requests
13
Merge Requests
13
Packages & Registries
Packages & Registries
Container Registry
Analytics
Analytics
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Commits
Issue Boards
Open sidebar
Why3
why3
Commits
a7ccb077
Commit
a7ccb077
authored
Feb 11, 2011
by
MARCHE Claude
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
option for displaying labels
parent
988ea15a
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
75 additions
and
0 deletions
+75
-0
examples/B_switch.why
examples/B_switch.why
+75
-0
No files found.
examples/B_switch.why
0 → 100644
View file @
a7ccb077
theory FSet
type elt
type t
logic single elt : t
logic union t t : t
logic mem elt t
(* triggers needed by Alt-Ergo but not Simplify, Z3 or CVC3 *)
axiom Mem_single : forall x y:elt [mem x (single y)].
mem x (single y) <-> x=y
axiom Mem_union : forall x:elt, s1 s2:t [mem x (union s1 s2)].
mem x (union s1 s2) <-> mem x s1 or mem x s2
end
theory Switch
(* useless
type enum_POSITION = Normal | Reverse | Void
*)
use import int.Int
logic in_1_3 (x:int) = 1 <= x <= 3
clone import FSet as S with type elt = int
logic f2 (m1:int) (m2:int) (m3:int) =
"`estimate preconditions in previous components'"
in_1_3 m1 and in_1_3 m2 and in_1_3 m3
logic f3 (m1:int) (m2:int) (m3:int) =
"`estimate preconditions in this component'"
in_1_3 m1 and in_1_3 m2 and in_1_3 m3 and
"`Local hypotheses'"
not (m1 = 2) and m1 = 1 and m2 = 2
logic f4 (m1:int) (m2:int) (m3:int) =
"`Check that the invariant (pos$1 = pos & pos$1 = pos) is preserved by the operation - ref 4.4, 5.5'" true
logic f5 (m1:int) (m2:int) (m3:int) =
(mem 1 (union (union (single m1) (single m2)) (single m3)) and
not 2 = m1 and not 2 = m2 and not 2 = m3 and
3 = 1)
or
(mem 2 (union (union (single m1) (single m2)) (single m3)) and
not 1 = m1 and not 1 = m2 and not 1 = m3 and
3=2)
or
((mem 1 (union (union (single m1) (single m2)) (single m3)) ->
mem 2 (union (union (single m1) (single m2)) (single m3))) and
(mem 2 (union (union (single m1) (single m2)) (single m3)) ->
mem 1 (union (union (single m1) (single m2)) (single m3))))
goal estimate1 : forall m1 m2 m3: int (* * POSITION *).
f2 m1 m2 m3 and f3 m1 m2 m3 -> f5 m1 m2 m3
logic f6 (m1:int) (m2:int) (m3:int) =
"`estimate preconditions in this component'"
in_1_3 m1 and in_1_3 m2 and in_1_3 m3 and
"`Local hypotheses'"
not(m1 = 2) and m1 = 1 and m3 = 2
goal estimate2 : forall m1 m2 m3: int (* * POSITION *).
f2 m1 m2 m3 and f6 m1 m2 m3 -> f5 m1 m2 m3
end
\ No newline at end of file
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