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
Iris
Iris
Commits
cb32a5f3
Commit
cb32a5f3
authored
Aug 19, 2016
by
Ralf Jung
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
docs: fix typo in pre-wp
parent
fd86b7bb
Pipeline
#2611
failed with stage
in 4 minutes and 10 seconds
Changes
1
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
1 addition
and
1 deletion
+1
-1
docs/model.tex
docs/model.tex
+1
-1
No files found.
docs/model.tex
View file @
cb32a5f3
...
...
@@ -107,7 +107,7 @@ $\textdom{wp}$ is defined as the fixed-point of a contractive function.
\begin{align*}
\textdom
{
pre-wp
}
(
\textdom
{
wp
}
)(
\mask
,
\expr
,
\pred
)
&
\eqdef
\Lam\rs
.
\setComp
{
n
}{
\begin{aligned}
\All
&
\rs
_
\f
, m,
\mask
_
\f
,
\state
. 0
\leq
m < n
\land
\mask
\disj
\mask
_
\f
\land
m+1
\in
\wsat\state
{
\mask
\cup
\mask
_
\f
}{
\rs
\mtimes
\rs
_
\f
}
\Ra
{}
\\
&
(
\All\val
.
\toval
(
\expr
) =
\val
\Ra
\Exists
\rsB
. m+1
\in
\pred
(
\rsB
)
\land
m+1
\in
\wsat\state
{
\mask
\cup
\mask
_
\f
}{
\rsB
\mtimes
\rs
_
\f
}
)
\land
{}
\\
&
(
\All\val
.
\toval
(
\expr
) =
\val
\Ra
\Exists
\rsB
. m+1
\in
\pred
(
\
val
)(
\
rsB
)
\land
m+1
\in
\wsat\state
{
\mask
\cup
\mask
_
\f
}{
\rsB
\mtimes
\rs
_
\f
}
)
\land
{}
\\
&
(
\toval
(
\expr
) =
\bot
\land
0 < m
\Ra
\red
(
\expr
,
\state
)
\land
\All
\expr
_
2,
\state
_
2,
\expr
_
\f
.
\expr
,
\state
\step
\expr
_
2,
\state
_
2,
\expr
_
\f
\Ra
{}
\\
&
\qquad
\Exists
\rsB
_
1,
\rsB
_
2. m
\in
\wsat\state
{
\mask
\cup
\mask
_
\f
}{
\rsB
_
1
\mtimes
\rsB
_
2
\mtimes
\rs
_
\f
}
\land
m
\in
\textdom
{
wp
}
(
\mask
,
\expr
_
2,
\pred
)(
\rsB
_
1)
\land
{}&
\\
&
\qquad\qquad
(
\expr
_
\f
=
\bot
\lor
m
\in
\textdom
{
wp
}
(
\top
,
\expr
_
\f
,
\Lam\any
.
\Lam\any
.
\mathbb
{
N
}
)(
\rsB
_
2))
...
...
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