Almost all of my initial feedback

[dimecon]

I read the tutorial online (rems-project.github.io/cn-tutorial) and used the exercises.zip file linked there (../getting-started/tutorials), consulting the solutions in src/examples of this repo (which I had to find independently of the online tutorial).

Installation

• The "language server" and "VSCode plugin" links don't work

Basic usage

• The new CN state files differ from the tutorial in having multiple pages. An update and a bit more explanation of state files would help.

Pointers and simple ownership

• At the end of "Resource outputs", v1 should be P
• "poinbts" should be points
• "at least as good" doesn't need to be in code font
• Block "has no meaningful output" but in CN we still write take X = Block<T>(x) which can be confusing; perhaps clarify that X is unconstrained or such?

Ownership of compound objects

• cn verify exercises/transpose2.c gives:
  exercises/transpose2.c:19:9: error: Pointer p needs allocation ID
  ...
  (UB missing short message): UB_CERB004_unspecified__pointer_add

  The "needs allocation ID" error message is different than the usual "Missing resource" error we see earlier in the tutorial, and I don't see allocation IDs explained in the tutorial. I'm also wondering what the last line (with "UB missing short message") means?

Arrays and loops

• Reference page is missing the array_shift keyword
• Explain what is meant by a "ghost statement"
• Change "quantifier Q" to "quantified Q" or "(universally) quantified variable Q" or such
• Regarding array_load.broken.c precondition description, "between 0 and n" should be "between 0 and n - 1"
• Reference page is missing the extract keyword
• "is split into 1. ... 1. ..."
• Regarding add_two_array.c, emphasize the need to assume i != j...
• ...and perhaps explain that otherwise split_case i == j is needed and why (perhaps unrelated to the tutorial itself: can the "Out of bounds" error message be improved when the i != j assumption is omitted?)

Defining predicates

• Reference page is missing ptr_eq keyword
• "are,m"
• More explanation of the "better way" would be helpful

Allocating and deallocating memory

• "Prove a specification" should be "Provide a specification"
• src/examples/slf_ref_greater.c src/exercises/slf_ref_greater.c solution should have P < R not P <= R

Lists

• Reference page is missing is_null keyword
• "below.)" should be "below)."
• exercises/slf_length_acc.c needs no additional annotation (?)

Working with external lemmas

• exercises/slf_sized_stack.c does not seem to need to apply any external lemmas
• Omitting /*@ unfold Length(...); @*/ from push, pop, or top in the solution yields an uncaught exception (might want to make this its own issue in the CN repo) The problem was using Z3 version 4.8.12: updating it to 4.8.14 (as recommended by the installation instructions for CN) fixed this.

Imperative queues

• C.next should be F.next
• Reference page is missing addr_eq keyword
• Lines using addr_eq could use some explanation
• "part of QueuePTR" should be "part of QueuePtr_At"
• "recurive"
• "One thing you might find odd...": I find any return statements odd here. The push.c example works without any return. It is the pop.c example where the returns cannot be factored out (though it looks like there is a "unified" solution refactoring the code for one return)
• Reference page is missing apply keyword
• Reference page is missing alloc_id keyword
• Lines using alloc_id could use some explanation
• Occurrences of snoc in the main text should be Snoc to agree with the code listings
• Delete some "simply" and "simple" (these don't seem to add anything and they might make the reader feel bad if it does not seem simple)
• Is there a reason to write "sequence" rather than "list"?
• InqQueueFB should be QueueFB
• InqQueueAux should be QueueAux
• "this has not been shown to be possible": is this out of date (looks like a solution is in the repo: src/examples/queue/pop_unified.c)?
• Commenting out the line in pop.c using alloc_id seems not to have any effect

Doubly-linked lists

• "Imperative Queues" doesn't need to be in code font
• "what other are needed": others
• "left left part": delete a "left"
• "'del.prev'": add code font
• "Dll data structure itself" "DlList data structure itself": add code font to Dll

Airport simulation

• The first of the six specification properties has an extra newline so they display as 1, 1, 2, 3, 4, 5
• "Constants section above": which section?
• Also, Constants doesn't need code font
• The "solutions folder" does not seem to be linked anywhere in the online tutorial