CVS difference for ai12s/ai12-0187-1.txt

Differences between 1.1 and version 1.2
Log of other versions for file ai12s/ai12-0187-1.txt

--- ai12s/ai12-0187-1.txt	2016/06/03 03:23:03	1.1
+++ ai12s/ai12-0187-1.txt	2016/06/07 04:21:44	1.2
@@ -232,5 +232,64 @@
+From: Randy Brukardt
+Sent: Thursday, June 2, 2016  10:22 PM
+> > Aside: There's a general problem with preconditions/postconditions 
+> > as to how to declare properties that are unchanged by (most) routines.
+> > For instance, for the Vector container, most routines do not change 
+> > the length. One could imagine adding Container.Length = 
+> > Container.Length'Old to every postcondition, but that's nasty to 
+> > read (it adds a lot of clutter). But one needs that information in 
+> > order to reason about the property without peeking at the body (the 
+> > compiler or prover has to know that the length is unchanged by 
+> > calling Element [for instance] in order to propagate its knowledge 
+> > to a later precondition). Someone had the idea of having a global 
+> > property that gets added automatically to every postcondition unless 
+> > the same property is explicitly tested in the postcondition. That 
+> > would solve the problem, but how to define "same property being
+> > explicitly tested" is unclear. Should I try to put together a proposal
+> > on these lines??
+> Something along those lines seems like a good idea.  I have spent some 
+> time thinking along those lines, but I don't know the right answer(s).
+Well, unlike Bob, I'm happy to propose an answer even if I don't know if it
+is the right answer. ;-)
+The attached proposal [Version /01 of this AI - Ed.] covers all of the example
+cases that I've been able to think of. I suspect that it would break down if
+someone wanted very many "stable properties", but I'm unsure if the additional
+complexity to fix that would be worthwhile (one would have to support some
+method of defining subsets of properties that are exclusive).
+I apologize for inventing some terminology from air; there very well might be
+a term that reasonably covers this, but I have neither the time nor energy to
+figure out if others have tried to solve this problem. After all, this idea is
+rather a trial balloon to get a discussion started, not necessarily a finished
+answer to the problems of the world's Ada programmers.
+From: Tucker Taft
+Sent: Friday, June 3, 2016  8:44 AM
+Nice proposal!
+This is closely related to the notion of "frame conditions" which is a general
+problem in program verification.  The "frame" is the set of objects or
+properties that are potentially affected by an operation.  This issue is
+discussed a bit in the Wikipedia article titled "frame problem."  Unfortunately
+this Wikipedia article is not as helpful as it could be.
+We should also relate this to the "Global" aspect, and perhaps consider adding
+a "Modified" aspect which would effectively establish a frame condition.
+From: Tullio Vardanega
+Sent: Friday, June 3, 2016  8:48 AM
+Yes, I second.

Questions? Ask the ACAA Technical Agent