From 30af0340e37bcf6488605eae9c9b0f36ce55df6f Mon Sep 17 00:00:00 2001 From: Johannes Hostert <jhostert@ethz.ch> Date: Fri, 15 Nov 2024 12:49:27 +0100 Subject: [PATCH] more stuff on example 14 --- theories/tree_borrows/README.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/theories/tree_borrows/README.md b/theories/tree_borrows/README.md index 1a9f3c73..0b3b5935 100644 --- a/theories/tree_borrows/README.md +++ b/theories/tree_borrows/README.md @@ -59,8 +59,9 @@ Example 1 is similar to the one shown in `examples/unprotected/mutable_delete_re The one shown in Coq has two places where arbitrary unknown functions are called, and Example 1 is just a special case of that, if one instantiates these unknown functions correctly. We have not shown Example 14, but two examples similar to it: -* `examples/unprotected/shared_delete_read_escaped_coinductive.v` demonstrates reasoning in a loop. +* `examples/unprotected/shared_delete_read_escaped_coinductive.v` demonstrates reasoning in a while loop. But note that this does not insert a read if there is none. Also, the tag is not protected. * `examples/protected/shared_insert_read.v` demonstrates that reads can be inserted on protected tags. - +This shows that the program logic has all the reasoning primitives required for verifying Example 14, +so taht its verification would be straightforward, just needing combine the two reasoning principles. -- GitLab