News
Project 2: `noop_preserves_spec_view`, Project 1 results
Written on 05.02.2025 13:26 by Andrea Lattuada
Dear Students, please note that the proof function `noop_preserves_spec_view` uses the term `noop` to indicate that the distributed system state does not change, and this use of the term is unrelated to a `NoOp` step. This is also indicated by the function's pre- and post-conditions and by the comment on the function.
In the meantime, you should have received emails with your results on Project 1. The score is out of 20 points: 10 points is the minimum score to pass. Everyone who's submitted has passed, well done! The maximum scores for each graded sections are as follows (your score for each is in [[x]] in the feedback):
host transitions:
init: 2
grant: 3
receive: 3
safety property: 3
safety proof:
invariants: 4
init_implies_inv proof: 1
inv_inductive proof: 4