Update proof obligation generation wiki

[mortenhaahr]

Hi, Preparing for my exam, I've noticed that there is little documentation related to proof obligation in VDM++. Both in literature (Validated Designs for Object-oriented Systems mentions the word proof obligation once) and the wiki page. It would be nice to have more information related to such an important topic.

I suggest updating the wiki page to either refer to more documentation or to update the contents of the wiki page.

Things I've noticed about the wiki page:

• "Categories" section is incomplete. The category "map apply" is not mentioned (perhaps the only one?).
• A "Statuses" section similar to "Categories" would be great.
• An example where a function changes status would also be great.

I would contribute myself but I have not been able to find information related to these topics.

[nickbattle]

This is a fair point, and I'll try to add more detail to the wiki page. This "shortcoming" was noticed a while ago by the Language Board and a working group established to try to improve the situation - that is to have complete, ideally formalized documentation describing a complete set of proof obligations for the language dialects. Unfortunately, as you say, this information is currently lacking or spread thinly, so it is hard to obtain.

You may find this helpful: https://github.com/overturetool/language/issues/33

I'll definitely add the missing category to the wiki. The status field was added in anticipation of automated theorem proving. Currently, the tools are able to discharge POs that match very limited patterns (like x > 0 => x > 0), which are trivial. But you may know that we are working on an Isabelle language translation that would be able to discharge many more POs, and presumably update their statuses.

Thanks for the feedback. I'll let you know when I've tweaked the wiki, and further suggestions would be welcome!

[nickbattle]

I had a quick look at this. The map apply obligation was there, but it was called "legal map application". I've reworded it so that it matches the name that will appear on the GUI (which is in POType.java). That said, the wiki has 33 entries and there are 41 listed in POType :-) So I'll go through them later today, add the other missing cases, and reword them all to match their POType string.

I'll add some references to the documents/books mentioned in the working group thread too.

[nickbattle]

I've now updated the table, and included the complete list of POTypes (it looks like the table was based on an old version of POType, because the missing types were all at the end of the Java list).

I also added a section called Further Reading, with links to the two books and the LB working group issue.

As mentioned, I can't add an example of a status changing because we don't yet have a way to discharge POs (which the text says). But I added something to the description of the Status field, explaining that it can be Proved or Unproved.

Is there anything else we can add?

[mortenhaahr]

Thanks for your great and quick work, Nick.

I would suggest for the time being making it more clear that discharging POs currently isn't possible and that too much effort shouldn't be put into understanding the "status" field. Speaking as a student, this was not clear to me after reading the Wiki.

[nickbattle]

OK, I'll try to add that. It would probably help if the teaching staff pointed this out too(!), or are you investigating this by yourself?

[mortenhaahr]

I read your addition and I think it is much more clear. Thanks. To answer your question, I was investigating it myself after missing the lecture. Perhaps Peter mentioned it :-)