Recursive list reversal; verification of well-formedness only - #1127
Conversation
ankushdas
changed the title
| // RUN: %diff "%s.expect" "%t" | ||
|
|
||
| /* | ||
| Linked list with nested permissions, translated from the NPL example in |
There was a problem hiding this comment.
The comment does not match the PR description. Let us drop this comment entirely.
| // WF: lists are non-empty, the head node is in the map, and all reachable | ||
| // nodes are in the map (so the structure is self-contained). | ||
| function {:inline} WF(l: List): bool { | ||
| l->head is Some && |
There was a problem hiding this comment.
This conjunct indicates that l always has a first element. In that case, why not make the type of head Loc (since it is always Some)?
The other option is to leave the type signature unchanged and allow for empty lists also.
| l->head is Some && | ||
| Map_Contains(l->nodes, One(l->head->t)) && | ||
| Reachable(l->nodes, l->head, None()) && | ||
| InDomain(l->nodes, l->head) |
There was a problem hiding this comment.
If you rebase with respect to the latest master, you will find that Reachable property is part of InDomain. So you should be able to drop the conjunct on line 27.
| var result_nodes: Map (One Loc) (Node int); | ||
|
|
||
| call new_head, helper_out := ReverseHelper(l_in, None()); | ||
| List(helper_head, result_nodes) := helper_out; |
There was a problem hiding this comment.
You could possibly use the Path_Store API to write 140-141 more compactly.
| /// already-reversed prefix), then recurses on List(old_next, nodes). | ||
| /// Returns (new_head, bag-of-reversed-nodes); new_head is the original tail. | ||
| /// No new Loc is allocated: l_out->nodes->dom == l_in->nodes->dom. | ||
| pure procedure {:vcs_split_on_every_assert} ReverseHelper({:linear_in} l_in: List, |
There was a problem hiding this comment.
I thought we had decided that we will use two separate lists to do the job. We will keep removing items from one list and adding them to the reversed list.
2 participants
This is a recursive list reversal function, inspired from Reynolds' list reversal example. The property verified is only well-formedness, i.e., if the input list is well-formed, then the reversed list is also well-formed. It does not verify if the reversed list is actually a reverse of the original list.