CVS difference for ai05s/ai05-0186-1.txt

Differences between 1.8 and version 1.9
Log of other versions for file ai05s/ai05-0186-1.txt

--- ai05s/ai05-0186-1.txt	2010/02/25 05:01:43	1.8
+++ ai05s/ai05-0186-1.txt	2010/04/29 06:27:43	1.9
@@ -3522,3 +3522,117 @@
              Default_Global out => (null);
+From: Randy Brukardt
+Sent: Thursday, April 22, 2010  10:56 PM
+After the discussion in Burlington on AI05-0186-1, I was tasked with looking at
+simplifications for the model in order to retain the critical parts. Thinking
+about this did not quickly lead to a clear solution, so I decided to write up my
+thoughts in the form of a paper. I was hoping that would help crystallize my
+ideas, and it did.
+I've posted the finished paper in the grab bag of the site:
+It's 10 pages long, but I don't think it is particularly difficult reading (it's
+nothing like accessibility).
+I entitled the paper "Preconditions, abstraction, and compile-time analysis",
+but I could probably have used a number of different titles. "Preconditions"
+really is a stand-in for all contracts in the form of an expression;
+"compile-time analysis" is really a stand in for optimization and static
+checking and even proof to some extent.
+Anyway, we'll discuss the options at our subcommittee phone call next week;
+hopefully at least subcommittee members will read it by then.
+Comments and discussion are welcome of course. (I put a version number on the
+paper so I can fix the inevitable errors.)
+From: Yannick Moy
+Sent: Monday, April 26, 2010  1:04 AM
+Thank you Randy for this very good explanation of the solutions and trade-offs.
+I have understood a lot by reading it, and I'd like to share with you a
+different view of the possible interaction between expression functions on one
+side and global annotations on the other side.
+You say the goal of contracts is to be able to decide if "the result of the
+function is known to be the same for a given pair of calls", like the calls to
+Some_Pre in the code below, both in precondition and in the body of
+procedure Do_Something (X : T) with Pre => Some_Pre (X);
+procedure Do_Something (X : T) is
+  Do_Some_Preliminary_Things (X);
+  if not Some_Pre (X) then
+    raise Constraint_Error;
+  end if;
+  ...
+Not talking yet of concurrent accesses, there are two subprograms which control
+here the answer to your question: the function Some_Pre which is called in a
+contract, and the procedure Do_Some_Preliminary_Things which may invalidate this
+contract. Thus, the compiler (or static analyzer) needs to know enough about the
+behavior of each in order to answer your question. I think the same solution
+does not necessarily apply to both.
+I think that your proposed solution with expression functions deserves more than
+to be "a reasonable fall-back option should no agreement be found on other
+options". It could well be the best option to implement functions that are
+called in contracts, like Some_Pre. Let's compare the benefits and drawbacks:
+In the benefits column:
+1) Straightforward to use. It is the most natural abstraction of the expressions
+   that one would like to put in contracts.
+2) Compile-time checked purity. Here, I'm using "purity" as in purely functional
+   languages, as a synonym for no (writing) side-effects. It may still read any
+   accessible piece of data, but ...
+3) Compile-time known body. The compiler (or static analyzer) has access to the
+   implementation of this expression function. Hence it can perform a host of
+   analyzes that would not be possible otherwise, with great precision and no
+   additional cost to the user in terms of annotations. This is related to ...
+4) Part of specifications. Contracts should be part of specifications. They do
+   not tell the "how" but the "what" to compute. They allow separate
+   verification of code, which would not be possible if contracts depend on
+   functions implemented in the body of packages.
+5) Correspond to 99% of useful contracts. With the addition of if-expressions,
+   case-expressions and quantified-expressions, all contracts on the library of
+   containers in GNAT (which are presently implemented as assertions) could be
+   expressed as expression functions.
+In the drawbacks column:
+1) Restricted to expressions. You cannot call a procedure or a function that is
+   not an expression function. For example, the following precondition is not
+   expressible: the sum of elements of array parameter A is less than integer
+   parameter Max. (It could be expressed with lambda-expressions like in
+   functional languages.) One should note here that such contracts are not very
+   useful for analysis, as they are usually too complex to allow proving
+   anything automatically. (Even the sum example above fits in this category!)
+2) Not readily usable with existing functions. As you noted, this requires that
+   some functions are rewritten as expression functions. This seems like a small
+   price to pay when switching to contracts and contract-based analysis.
+So what about procedure Do_Some_Preliminary_Things? Here, the annotations for
+writing global objects are the best possible solution. They should make it
+possible to know if the expression designated by "Some_Pre (X)" is modified by
+calling Do_Some_Preliminary_Things.
+If you agree with this separation of concerns, then probably the focus of global
+annotations should change. In particular, this would not be true to say that
+"the current primary purpose of the annotations is to support precondition
+Some benefit of this separation is that the expression functions are readily
+understood and usable by Ada programmers, while global annotations provide an
+additional benefit for those who will take the time to understand them.
+Although I'm in favor of a way to express the "frame condition" of a subprogram,
+I'll leave this discussion for now, to separate concerns. :)

Questions? Ask the ACAA Technical Agent