Commit graph

495 commits

Author SHA1 Message Date
Adam Chlipala
a4cc213b75
Merge pull request #42 from samuelgruetter/messages_typo
typo
2021-01-03 14:41:11 -05:00
Adam Chlipala
845c9189c1
Merge pull request #51 from mdempsky/csl-example-typo
Fix typo in ConcurrentSeparationLogic.v example
2021-01-03 14:39:16 -05:00
Adam Chlipala
7db4d122d4
Merge pull request #50 from mdempsky/loop-typo
Fix typos in operational semantics for "Loop" command
2021-01-03 14:38:45 -05:00
Matthew Dempsky
509ebb1d06 Fix typo in ConcurrentSeparationLogic.v example
In the 3-stage example, the middle stage moves list elements from the
first stack to the second stack, not back onto the first stack again.
2020-09-24 13:30:58 -07:00
Matthew Dempsky
bd92c1cbb3 Fix typos in operational semantics for "Loop" command
In section 13.3, the type of Loop is defined as:

    Loop : forall a, a -> (a -> cmd (outcome a)) -> cmd a

However, the operational semantics provided in sections 14.1 and 18.1
invoke the loop body function using "Again(i)" (type "outcome a").
They should instead use simply "i" (type "a").

Changing to "f(i)" also matches the StepLoop formalizations in
SeparationLogic.v and ConcurrentSeparationLogic.v, which invoke simply
"body init" (rather than "body (Again init)").
2020-09-24 11:43:41 -07:00
Adam Chlipala
e32105c142
Merge pull request #48 from mdempsky/sepcancel-typo
Add missing parentheses in SepCancel's normalize2 tactic
2020-07-25 09:18:19 -04:00
Matthew Dempsky
0a55c03aa0 Add missing parentheses in SepCancel's normalize2 tactic
Before this change, "Print normalize2" prints:

    Ltac Frap.SepCancel.Make.normalize2 :=
      match goal with
      | |- context [ (?p * lift) (?P /\ ?Q) ] => rewrite (lift_uncombine p P Q)
      | |- context [ ?p * (?q * ?r) ] => rewrite (star_assoc p q r)
      end

After, it prints:

    Ltac Frap.SepCancel.Make.normalize2 :=
      match goal with
      | |- context [ ?p * [|?P /\ ?Q|] ] => rewrite (lift_uncombine p P Q)
      | |- context [ ?p * (?q * ?r) ] => rewrite (star_assoc p q r)
      end
2020-07-24 18:23:44 -07:00
Adam Chlipala
d1ace360eb Parenthetical remarks to characterize in what senses various analysis results are 'most precise' (closes #47) 2020-05-22 17:10:37 -04:00
Adam Chlipala
b8d0cefa6a Consistency of notation for implication (closes #46) 2020-05-11 11:50:09 -04:00
Adam Chlipala
b214d2c78a Revising before class 2020-05-10 14:10:01 -04:00
Adam Chlipala
8a87c209f7 Revising before class 2020-05-05 19:26:59 -04:00
Adam Chlipala
1c91cf3d5c Merge branch 'master' of github.com:achlipala/frap 2020-04-29 16:06:34 -04:00
Adam Chlipala
c2bbf00999 Update for latest Coq version 2020-04-29 14:29:58 -04:00
Adam Chlipala
5f735225ef Revising before class 2020-04-28 09:40:40 -04:00
Adam Chlipala
300f78191e Revising before class 2020-04-26 14:30:18 -04:00
Adam Chlipala
42d5af6d2d Revising before class 2020-04-26 14:29:53 -04:00
Adam Chlipala
213f8b270b Revising before class 2020-04-26 14:28:52 -04:00
Adam Chlipala
e56390f108 Update SessionTypes to follow changes in MessagesAndRefinement 2020-04-24 11:15:51 -04:00
Adam Chlipala
a8dd970c96
Merge pull request #44 from samuelgruetter/message_passing_fixes
Message passing fixes
2020-04-24 09:50:30 -04:00
Adam Chlipala
eccb504f08
Merge pull request #43 from bkushigian/master
Change overloaded term `S` in section 5.4
2020-04-24 09:29:23 -04:00
Samuel Gruetter
26b8436e0c fix warnings in MessagesAndRefinement.v 2020-04-21 19:22:39 -04:00
Samuel Gruetter
ceddf6d6e4 the few keystrokes saved by using a Coercion from action
to label is not worth the confusion it creates for students
during proofs
2020-04-21 19:19:22 -04:00
Samuel Gruetter
6a1e7fa644 also replace Set by Type in LStepSend and LStepRecv 2020-04-20 21:42:33 -04:00
bkushigian
22f3238a8a Change overloaded term S in section 5.4 2020-04-20 09:34:30 -07:00
Adam Chlipala
69de20dec8 Revising before class, including with an optimization to the model-checking engine 2020-04-20 11:56:23 -04:00
Adam Chlipala
c607913898 Typo in translation rule 2020-04-15 09:48:24 -04:00
Adam Chlipala
d74a0ebb42 Revising before class 2020-04-14 15:48:36 -04:00
Adam Chlipala
2efec7b61d Typo fix 2020-04-14 11:55:26 -04:00
Samuel Gruetter
ce1bc740c4 allow Type instead of just Set in Send and Recv
so that we can send fmaps
2020-04-13 15:26:11 -04:00
Adam Chlipala
b632c66f85 More revision before class 2020-04-13 09:27:45 -04:00
Samuel Gruetter
1cc82281bf typo 2020-04-12 21:36:38 -04:00
Adam Chlipala
8a554ded4c Revising SeparationLogic before class 2020-04-11 14:33:14 -04:00
Adam Chlipala
000c22f7f1 Merge branch 'master' of github.com:achlipala/frap 2020-04-08 10:48:27 -04:00
Adam Chlipala
ca3a490119 Revising before class 2020-04-08 10:48:14 -04:00
Adam Chlipala
da53b28584 HoareLogic_template: hint databases 2020-04-06 14:25:19 -04:00
Adam Chlipala
583605fded Merge branch 'master' of github.com:achlipala/frap 2020-04-05 09:30:12 -04:00
Adam Chlipala
477788abaa Missed loop invariant in big-step semantics 2020-04-05 09:30:01 -04:00
Adam Chlipala
75c04e1448
Merge pull request #40 from samuelgruetter/hoare_triple_big_step_while
explain hoare_triple_big_step_while
2020-04-02 08:19:54 -04:00
Samuel Gruetter
1c97e1a389 explain hoare_triple_big_step_while 2020-04-01 21:49:00 -04:00
Adam Chlipala
7bc0425ccf
Merge pull request #39 from bkushigian/patch-1
Fixed markdown inline
2020-03-29 10:20:51 -04:00
Ben A Kushigian
01ad154c5a
Fixed markdown inline
was
```
`make lib'
```
should be
```
`make lib`
```
2020-03-28 15:07:21 -07:00
Adam Chlipala
b5e1ae0c29 Clarify what linear_arithmetic does these days 2020-03-17 15:50:19 -04:00
Adam Chlipala
72c0bc3a04
Merge pull request #38 from mdempsky/parity-subtract
Add missing "O - O = E" abstraction case
2020-03-17 11:24:57 -04:00
Adam Chlipala
c502399de4 Separate out library code with its own license 2020-03-17 09:22:06 -04:00
Matthew Dempsky
ebcd23ee6c Add missing "O - O = E" abstraction case
This case is implemented by parity_subtract in
AbstractInterpretation.v and is necessary to calculate the "most
precise abstraction."

See also #28, #37.
2020-03-16 12:58:20 -07:00
Adam Chlipala
51a7fae33e Unnecessary Fixpoint 2020-03-11 09:40:55 -04:00
Adam Chlipala
dd266f2d8c Proofreading and Coq-version-updating AbstractInterpretation 2020-03-07 15:32:50 -05:00
Adam Chlipala
64fe989cdb Turn off some warnings 2020-03-04 11:51:34 -05:00
Adam Chlipala
19d915fb37
Merge pull request #36 from samuelgruetter/ltac_lecture_comment
explain why recursive [inster] can fail
2020-03-02 11:45:36 -05:00
Samuel Gruetter
74e2399343 explain why recursive [inster] can fail 2020-03-01 22:30:35 -05:00