Closed jhoenicke closed 1 year ago
This adds a ghost variable to each owner that counts the elements behind it in the list, and proves the invariant that the counts are correct. It then shows that ownerCount corresponds to the count of the head element of the list.
This adds a ghost variable to each owner that counts the elements behind it in the list, and proves the invariant that the counts are correct. It then shows that ownerCount corresponds to the count of the head element of the list.