pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-10 08:17:52 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Merge pull request #23 from k4rtik/master

Browse source 
Some typo fixes
This commit is contained in:
Adam Chlipala 2018-04-01 14:29:31 -04:00 committed by GitHub
commit 5c5cfd9600
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
SeparationLogic.v
View file

@ -93,7 +93,7 @@ Definition trsys_of (h : heap) {result} (c : cmd result) := {|
|}. |}.
(* Now let's get into the first distinctive feature of separation logic: an (* Now let's get into the first distinctive feature of separation logic: an
* assertion language that takes advantage of *pariality* of heaps. We give our * assertion language that takes advantage of *partiality* of heaps. We give our
* definitions inside a module, which will shortly be used as a parameter to * definitions inside a module, which will shortly be used as a parameter to
* another module (from the book library), to get some free automation for * another module (from the book library), to get some free automation for
* implications between these assertions. *) * implications between these assertions. *)

2
SharedMemory.v
View file

@ -448,7 +448,7 @@ Qed.
* shared state identically. In such a case, we may always pick our favorite * shared state identically. In such a case, we may always pick our favorite
* thread to step next. *) * thread to step next. *)
(* To make all that formal, we will do some static program analyze to summarize (* To make all that formal, we will do some static program analysis to summarize
* which atomic actions a thread might take. *) * which atomic actions a thread might take. *)
Record summary := { Record summary := {
Reads : set nat; Reads : set nat;