Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Marianna Rapoport
iris-coq
Commits
4cf90c36
Commit
4cf90c36
authored
Mar 15, 2016
by
Ralf Jung
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
markdown README
parent
14258ee6
Changes
2
Hide whitespace changes
Inline
Side-by-side
Showing
2 changed files
with
34 additions
and
1 deletion
+34
-1
README.md
README.md
+33
-0
program_logic/weakestpre.v
program_logic/weakestpre.v
+1
-1
No files found.
README
→
README
.md
View file @
4cf90c36
PREREQUISITES
-------------
# PREREQUISITES
This version is known to compile with:
...
...
@@ -12,9 +11,23 @@ fetch the development branch yourself). Iris compiles fine even without this
patch, but proof bullets will only be in 'strict' (enforcing) mode with the
fixed version of Ssreflect.
BUILDING INSTRUCTIONS
---------------------
# BUILDING INSTRUCTIONS
Run the following command to build the full development:
make
# STRUCTURE
*
The folder
`prelude`
contains an extended "Standard Library" by Robbert
Krebbers
<http://robbertkrebbers.nl/thesis.html>
.
*
The folder
`algebra`
contains the COFE and CMRA constructions as well as
the solver for recursive domain equations.
*
The folder
`program_logic`
builds the semantic domain of Iris, defines and
verifies primitive view shifts and weakest preconditions, and builds some
language-independent derived constructions (e.g., STSs).
*
The folder
`heap_lang`
defines the ML-like concurrent heap language, and a
few derived constructions (e.g., parallel composition).
*
The folder
`barrier`
contains the implementation and proof of the barrier.
*
The folder
`examples`
contains the examples given in the paper.
program_logic/weakestpre.v
View file @
4cf90c36
...
...
@@ -248,7 +248,7 @@ Proof. by setoid_rewrite (always_and_sep_r _ _); rewrite wp_frame_r. Qed.
Lemma
wp_impl_l
E
e
Φ
Ψ
:
((
□
∀
v
,
Φ
v
→
Ψ
v
)
∧
WP
e
@
E
{{
Φ
}})
⊢
WP
e
@
E
{{
Ψ
}}.
Proof
.
rewrite
wp_always_l
;
apply
wp_mono
=>
//
v
.
rewrite
wp_always_l
.
apply
wp_mono
=>
//
v
.
by
rewrite
always_elim
(
forall_elim
v
)
impl_elim_l
.
Qed
.
Lemma
wp_impl_r
E
e
Φ
Ψ
:
...
...
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