Commit 360187b3 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Fix citations.

parent 4499cf49
...@@ -130,11 +130,13 @@ ...@@ -130,11 +130,13 @@
publisher={ACM} publisher={ACM}
} }
@misc{gueneau2021theorems, @article{gueneau2021theorems,
title={Theorems for Free from Separation Logic Specifications}, title={Theorems for Free from Separation Logic Specifications},
author={Anonymous}, author={Birkedal, Lars and Dinsdale-Young, Thomas and Guéneau, Armaël and Jaber, Guilhem and Svendsen, Kasper and Tzevelekos, Nikos},
year={2021}, journal = pacmpl,
note={Under submission at ICFP'21} volume = "5",
number = "ICFP",
year={2021}
} }
@inproceedings{zakowski2018verified, @inproceedings{zakowski2018verified,
......
...@@ -58,7 +58,7 @@ would be unable to open their invariant around the triples shown ...@@ -58,7 +58,7 @@ would be unable to open their invariant around the triples shown
in~\fref{fig:queue:spec:seq}. in~\fref{fig:queue:spec:seq}.
Yet these operations are ``atomic'' in some empirical sense. Yet these operations are ``atomic'' in some empirical sense.
The concept of logical atomicity~\cite[\S7]{jung-slides-2019,iris-15} aims at addressing that difficulty. The concept of logical atomicity~\cite[\S7]{jacobs2011expressive,jung-slides-2019,iris-15} aims at addressing that difficulty.
To use it, we substitute ordinary Hoare triples with \emph{logically atomic triples}. To use it, we substitute ordinary Hoare triples with \emph{logically atomic triples}.
Just like ordinary triples, they specify a program fragment with a precondition and a postcondition. Just like ordinary triples, they specify a program fragment with a precondition and a postcondition.
The core difference is that invariants can be opened around a logically atomic triple, regardless of the number of execution steps of the program fragment: in a sense, when a function is specified using a logically atomic triple, one states that said function behaves as if it were atomic. The core difference is that invariants can be opened around a logically atomic triple, regardless of the number of execution steps of the program fragment: in a sense, when a function is specified using a logically atomic triple, one states that said function behaves as if it were atomic.
......
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