Increasing Confidence in Implicit Function Definition

Formalizing the user's requirements can be a painstaking task. Even if the (human) specifier perfectly understands what the customer actually wants, he or she is not safe from committing specification errors which may have a major impact on the properties of the very system formalized. In the development of part of an access control system using the formal development method VDM (see [Jones]) and its specification language VDM-SL, a particular specification error has occurred repeatedly.
We propose an extension of VDM such that this type of error is less likely to be made.

In model-oriented specifications, implicit function definition provides a powerful means of expressing functionality without referring to a particular implementation. According to an implicit function definition, once a function terminates, some relation between the input and the output (the "postcondition") is required to hold. Moreover, the function is only required to return a well-defined result if a certain restriction on the input parameters (the "precondition") is satisfied.
Since both pre- and postconditions are logical expressions, they usually contain a number of predicates. Clearly, the "relationship" between a function and "its" predicates has a major influence on the correctness of the very system formalized. This "usage" can be looked upon in two ways. The building blocks, which remain the same in both cases , are functions and predicates. The difference can be found in the way how they are related: between functions and predicates

1. there is a one-to-many "uses" relation.This corresponds to the traditional way of (implicitly) defining a function: one function contains many predicates.
2. there is a many-to-one "uses" relation putting in context those functions by which the predicate is used and the predicate itself.

From now on, we will view part of an example specification from three different perspectives. The first view on functions and predicates follows the two relations introduced above. Assume that the predicates in the implicit definition of some function myfun1 are pred1, pred2, pred3, pred4, pred6,etc.In other words, for one function there are a number of predicates. Concerning the second relation, suppose that predicate pred1 is also used by functions myfun2, myfun3, myfun5, etc. Thus, one predicate is related to a number of functions:

              pred1     myfun1  
              pred2     myfun2 
myfun1 "uses" pred3     myfun3 "uses" pred1
              pred4     myfun5
              pred6      ... 
               ...    

      1   :   many         many  :   1
       relation              relation

In a typical formal specification, simply by looking at the function's pre- and postcondition it can easily be found out which predicates are involved in an implicit function definition. On the other hand, in order to find out which functions make use of a particular predicate, the whole of the specification needs to be inspected. We believe that this complication has favored the kind of specification error mentioned above: unintentional substitution or omission of a predicate.
In consequence, we will make a proposal for an extension of model-oriented specification languages like VDM-SL such that the "lacking" relationship can easily be included. The modification will be based on an explicit naming of those functions by which a particular predicate is used. Due to the predicate oriented view, the definition will be called a "predicate oriented definition" (POD).

The second way of viewing part of our example specification follows the traditional implicit specification style. Coming back to the specification error mentioned above, we will now illustrate that minor structural changes may have a significant impact on the properties of the system formalized. Function myfun1 is taken from our example specification and myfun2 is meant to have the same functionality as myfun1. However, there is a difference between the two functions: a predicate has (unintentionally) been replaced by another one, which is not quite easy to spot even when choosing a better naming convention:

 
functions  
 myfun1(par1:type1, par2:type2, par3:type3) res:type4
  pre  pred1(par1)      and pred2(par2,par3) and    
       pred4(par1,par2)  
  post pred3(par1,res)  and pred6(res) and 
       pred9(par3,res)  and pred8(par2,res);

 myfun2(par1:type1, par2:type2, par3:type3) res:type4
  pre  pred1(par1)      and pred2(par2,par3) and 
       pred4(par1,par2)         
  post pred3(par1,res)  and pred7(res) and   
       pred9(par3,res)  and pred8(par2,res);  

In the third way of viewing part of the example specification we will make use of our new predicate oriented approach. As it has been said before, it is related to one predicate . In the most simple form, the POD lists all functions by which some predicate is used, with occurances in pre- and postconditions kept separate. As myfun2 was originally meant to have the same functionality as myfun1, we would expect myfun1 and myfun2 to appear in PODs for one predicate together or not at all. Obviously, this is not the case in the POD of predicates pred6 and pred7. It is formally stated that pred6 occurs in the pre-condition of function myfun1 but not in myfun2. pred6 is also used in the postcondition of function myfun3. pred7, on the other hand, is part of the precondition of function myfun2 and there is no function with pred7 in its postcondition:

  
  pred6  
    in-pre {myfun1}    
    in-post {myfun3} 

  pred7      
    in-pre {myfun2} 
    in-post {}  

Though this most basic style clearly identifies all functions making use of a predicate, it does not provide enough information to even find out whether the predicate occurs negated or non-negated. There are various possibilities of including more information in the POD:

• include how the predicate is used by the function (which is a generalized form of whether it appears negated or non-negated)
• include which of the function's parameters are used by the predicate
• ...

We would like to emphasize that a POD construct is no definition of a predicate. Rather, it can be considered to contribute to function definition. It might even be used to replace a traditional function definition. This leads us to a discussion of what we expect to gain from our new notation and of how to integrate it into the software development process:
One possibility is increasing confidence in implicit function specification by defining functions in both traditional and POD style. Subsequently, a consistency check can be performed. Obviously, the two-track specification enhances the degree of redundancy in the specification.
As the degree of redundancy increases (and so does specification effort), a more rigorous consistency checking can be performed.

For integrating our new approach into the VDM software development method, first, the specification language VDM-SL needs to be extended by a POD construct.
Second, we need to find a way of imposing equivalence between the two representations.
An integral part of formal software development are so-called proof-obligations which formally express what needs to be proven. All we need to do is generate additional proof-obligations which will be submitted to an automatic theorem prover. Proof-obligations are given in Hilbert-style, and as such they consist of a set of premises and a conclusion. For a discussion of proof-obligations in the VDM development process see [Jones]. Proof-obligations for consistency are discussed for instance in [Aichernig].

Our double-track definition can easily be turned into proof-obligations mechanically: let POD-SET be the set of all PODs in a form similar to the one sketched above, let pod-p denote one particular POD for some predicate p, let in-pre-p denote the set of (references to) functions using predicate p in the precondition and let pre-f denote the precondition of a particular function f. If the preconditions simply consist of a conjunction of predicates, we expect the following to hold:

      f:function; p:predicate; pod-p in set POD-SET;
      f in set in-pre-p
      -----------------------------------------------------
           pre-f => p

Informally, this proof-obligation requires that for each function mentioned by set in-pre of a POD there must be a corresponding implicit function definition where the predicate is used in the precondition. In the same manner, we can construct a proof-obligation imposing that for each traditional function definition there must be a POD. This principle applies equally to postconditions.

References

[Aichernig] Aichernig, B. K.; Larsen P. G.; A Proof Obligation Generator for VDM-SL, in John Fitzgerald and Cliff B. Jones and Peter Lucas, editors, FME'97: Industrial Applications and Strengthened Foundations of Formal Methods (Proc. 4th Intl. Symposium of Formal Methods Europe, Graz, Austria, September 1997), volume 1313 of Lecture Notes in Computer Science, Springer-Verlag, 1997

[Jones] Jones, C. B.; Systematic Software Development Using VDM, second edition, Prentice-Hall International, 1990