|
|
|
|
|
|
||
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Issue: 7.6 Status: Definitive
DOCTYPE:Praxis title:varchar=title reference:varchar=reference status:varchar=status issue:varchar=issue date:varchar=date projectname:varchar=DocumentSet Issue 7.6, Definitive, 2nd February 2009 000_000 Generation of PFs for SPARK Programs
|
|
|
|
Originator |
|
|
|
|
|
|
|
Approver |
|
|
|
SPARK Team Line Manager |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
||
|
|
The contents of this manual are the subject of copyright and all rights in it are reserved. The manual may not be copied, in whole or in part, without the written consent of Praxis High Integrity Systems Limited.
Limited Warranty
Praxis High Integrity Systems Limited save as required by law makes no warranty or representation, either express or implied, with respect to this software, its quality, performance, merchantability or fitness for a purpose. As a result, the licence to use this software is sold ‘as is’ and you, the purchaser, are assuming the entire risk as to its quality and performance.
Praxis High Integrity Systems Limited accepts no liability for direct, indirect, special or consequential damages nor any other legal liability whatsoever and howsoever arising resulting from any defect in the software or its documentation, even if advised of the possibility of such damages. In particular Praxis High Integrity Systems Limited accepts no liability for any programs or data stored or processed using Praxis High Integrity Systems Limited products, including the costs of recovering such programs or data.
SPADE is a registered trademark of Praxis High Integrity Systems Limited.
Note: The SPARK programming language is not sponsored by or affiliated with SPARC International Inc. and is not based on SPARC™ architecture.
2.2 Historical background and current uses
3 The Language of Path Functions
5 Generation of Path Functions
6 Simplification of Path Functions
Document Control and References
Contents
This manual explains the process of generating path functions (PFs) for SPARK programs together with their format and interpretation. Details of the use of the SPARK Examiner, such as command line switches and error messages, are contained in the manual “SPARK Examiner User Manual”. The use of the SPADE Automatic Simplifier is described separately, in other Praxis High Integrity Systems documents.
Although it can sometimes be effective, path function analysis has significant disadvantages as compared with use of verification conditions. Users are advised to read the section “Disadvantages” below and consider alternative forms of analysis before embarking on large V&V programs.
Path functions can be considered as a form of serial to parallel transformation of a sequence of program statements. Instead of a sequence of statements, typically containing branches and conditions, we produce a flow graph and identify all possible paths through it. Each of these paths will have associated with it a “traversal condition” which is a Boolean expression stating the conditions under which that path will be taken and a set of mapping statements showing the transformations to the program variables that will occur on that path.
Consider the following small procedure which calculates its single out parameter from its three in parameters.
procedure Max(W, X, Y : in Integer;
Z : out Integer)
--# derives Z from W, X, Y;
is
T : Integer;
begin
T := W + X;
if T > Y then
Z := T;
else
Z := Y;
end if;
end Max;
The flow graph for this program is as follows
From the start to the finish of this subprogram their are clearly two paths. One will be traversed if W + X > Y and the other if not(W + X > Y). The mapping for the former path is Z := W + X and for the latter Z := Y;.
The PFs generated are as follows (the value assigned to the variable on the left will be its final value).
Statement: start 1 successor(s)
Successor statement: finish.
Path 1
Traversal condition:
1: w + x > y .
Action:
z := w + x &
t := w + x .
Path 2
Traversal condition:
1: not (w + x > y) .
Action:
z := y &
t := w + x .
2.2 Historical background and current uses
Path function analysis (PFA) evolved during the 1970s in response to the need to understand large amounts of existing code by a process of reverse engineering. It remained popular for the retrospective analysis of critical software largely because it was one of the few static analysis techniques capable of revealing the semantics of existing code which generally had not been written with demonstration of correctness as a primary objective. Some uses of PFA ¾ e.g. showing that exported variables are assigned values on all subprogram paths ¾ are better performed by information flow analysis; however, PFA has some utility in the following areas:
· Revealing structural complexity in code by directly showing the number of paths through a program segment.
· Showing that intended values are written to exported variables on all paths.
· Showing informally that variables controlling loops are modified in a way that will ensure loop termination occurs.
PFA has a number of significant disadvantages that greatly reduce its usefulness.
PFA is inherently backward-looking. Code is first written, then its “specification” is obtained in the form of path functions and finally these are informally compared with some “requirement”. This process falls well short of current best practice (as espoused, for example, in Def Stan 00-55) which emphasizes the need for a forward train of reasoning from requirement to specification to code which is much better served by proof technology.
PFA can produce very large volumes of output which need to be read, interpreted and configuration controlled. The size of each mapping statement is governed by the number of variables being assigned but the total output multiplies this by the number of paths (which increases exponentially with the number of branching statements) each of which may also have a complicated traversal condition. The volume of output can be such that its informal examination is more costly than the more rigorous construction of proofs would be.
2.3.3 Difficulty of interpreting loops
The presence of loops complicates interpretation of path functions because the control flow graph of a loop has to be “cut” in the loop body, generating paths to the loop head, around the loop, and from each exit point. This means that it is usually no longer possible readily to determine the final values of variables because they now depend on the combination of paths used to reach the subprogram end. Consider the following naive function algorithm use to calculate an integer power:
7 function Power(X, Y : Natural) return Natural
8 is
9 T : Natural;
10 begin
11 T := 1;
12 for I in Natural range 1..Y loop
13 T := T * X;
14 end loop;
15 return T;
16 end Power;
The (simplified) path functions for this are as follows:
Statement: start 2 successor(s)
Successor statement: line 12.
Path 1
Traversal condition:
1: 1 <= y .
Action:
t := 1 &
i := 1 .
Successor statement: finish.
Path 1
Traversal condition:
1: y < 1 .
Action:
power := 1 &
t := 1 .
Statement: line 12 2 successor(s)
Successor statement: line 12.
Path 1
Traversal condition:
1: i <> y .
Action:
t := t * x &
i := i + 1 .
Successor statement: finish.
Path 1
Traversal condition:
1: i = y .
Action:
power := t * x &
t := t * x .
Path functions are generated:
· from the start of the subprogram to the start of the loop (line 12) and to the finish (if the loop is not entered); and
· from the loop head to itself (loop not yet terminated) and from the loop head to the finish.
From these it is possible to see that if y (the power) is zero then the correct value 1 is returned (note the use of the function name to denote the value returned by the function). It is also possible to see that each time around the loop the temporary variable t is multiplied by x and that the loop counter i is incremented; however, it is not possible readily to see that from start to finish the returned value is x**y. This conclusion can only be reached by considering the paths from line 12 to itself and from line 12 to the finish in combination. (By contrast, proof of this function allows the behaviour of the loop and of the subprogram as a whole to be considered separately from one another).
2.3.4 Difficulty in interpreting procedure calls
Where, as is typically the case, a subprogram calls other subprograms in the course of its execution, further difficulties in interpretation of PFA arise. The values exported by the calls to a procedure subprogram are represented in the mapping statement by a series of functions each returning one export which is obtained from all the imports on which it depends. (See below for more information on these modelling functions.) The interpretation is either in terms of the perhaps overly abstract representation of the operations performed by the called procedure or it requires the analyst to “mentally inline” the called procedure. For example, a mapping statement which was expected to show that a variable was incremented might, if the incrementing was done via a procedure call, show x := inc(x); the correctness of which depends on a knowledge of the semantics of procedure Inc. Again proof has the advantage of being able consider both Inc and the subprogram which calls it in isolation.
The final but highly significant disadvantage or PFA is that it is essentially an informal process. An analyst can do nothing more than study the output and document any observations that arise. There is no auditable equivalent of a proof log.
The disadvantages listed above can be largely obviated by adoption of proof as described in “The Generation of Verification Conditions for SPARK Programs”. Even where a specification suitable for use as proof contexts in the SPARK program are not available, considerable assurance can be gained by the use of proof to show the program to be free of run-time errors. The specific uses of PFA outlined earlier can often be achieved more cleanly by proof involving only minimal additional annotations or by use of the VC Generator in an interrogative manner.
3 The Language of Path Functions
Path functions are expressed in FDL on to which SPARK constructs are mapped exactly as described in “The Generation of Verification Conditions for SPARK Programs”. Their form differs from that described for VCs only as follows.
VCs contain only expressions, not statements. PFs contain multiple assignment statements of the following form:
t := t * x &
i := i + 1 .
The clauses separated by & can be considered to be simultaneous assignments of their right hand sides to the variable on the left.
If a procedure P has a dependency relation
derives E1 from I11, I12, ... , I1m &
E2 from I21, I22, ... , I2m &
..............................
En from In1, In2, ... , Inm;
then a statement calling P is modelled by a multiple assignment involving the simultaneous application of n implicitly-declared proof functions named P__suffix (where suffix is the name of the formal parameter or global variable export returned by that modelling function):
E1 := P__E1(I11, I12, ... , I1m) &
E2 := P__E2(I21, I22, ... , I2m) &
....................................
En := P__En(In1, In2, ... , Inm);
Where the exports En and imports Inm are parameters. The actual parameter name is substituted into these modelling functions; the names of global variables are unchanged.
For example the following code shows a simple procedure which doubles its integer parameter. This procedure is used to define another which multiplies its parameter by four.
procedure Double(X : in out Integer)
--# derives X from X;
is
begin
X := X * 2;
end Double;
procedure Quad(X : in out Integer)
--# derives X from X;
is
begin
Double(X);
Double(X);
end Quad;
The PFs generated for procedure Quad are as follows:
Statement: start 1 successor(s)
Successor statement: finish.
Path 1
Traversal condition:
1: true .
Action:
x := double__x(double__x(x)) .
Showing the successive applications of the implicitly declared function double__x which model the successive call to procedure Double.
Where the called procedure references an external variable of mode in, an additional proof function models the volatility of the input. The effect is that the external variable is treated as an export as well as an import. If the called procedure updates an external variable of mode out, an extra parameter is added to the proof function to show that the state of the external variable depends on itself (i.e. the history of values written). The effect is that the external variable is treated as an import as well as an export.
The following example shows the generation of PFs from procedure PerformModeOperation of the heating controller example detailed in “The Generation of Verification Conditions for SPARK Programs”.
procedure PerformModeOperation
--# global Heating, Mode, AboveTemp, Time;
--# derives Heating from Mode, AboveTemp, Time;
is
begin
case Mode is
when ModeSwitch.off => Heating := False;
when ModeSwitch.cont => Heating := not AboveTemp;
when ModeSwitch.timed => Heating := not AboveTemp and
IsInOperatingPeriod(Time);
end case;
end PerformModeOperation;
In this small example, informal correspondence between the PFs and the Z specification is clear.
Statement: start 1 successor(s)
Successor statement: finish.
Path 1
Traversal condition:
1: mode = modeswitch__off .
Action:
heating := false .
Path 2
Traversal condition:
1: mode = modeswitch__cont .
Action:
heating := not abovetemp .
Path 3
Traversal condition:
1: mode = modeswitch__timed .
Action:
heating := (not abovetemp) and
isinoperatingperiod( time) .
5 Generation of Path Functions
Path function generation may be selected using the PFS command line switch (/pfs on Windows, -pfs on SUN or Linux). Two files are produced for each well-formed subprogram: a file of FDL declarations with the extension .DEC and a file of path functions with the extension .PFS. These are the equivalent of the .FDL and .VCG files produced when VC generation is selected. The file names and locations used are as described in the “SPARK Examiner with VC Generator User Manual”. The files produced, and relationships with the SPADE Simplifier tool are shown in the following diagram.
6 Simplification of Path Functions
Path functions can be simplified by the SPADE Automatic Simplifier. As well as the general improvement in presentation of expressions within the PF, the Simplifier may identify contradictions in the traversal conditions for a path. Such paths are non-executable and are removed by the Simplifier.
Document Control and References
Praxis High Integrity Systems Limited, 20 Manvers Street, Bath BA1 1PX, UK.
Copyright Praxis High Integrity Systems Limited 2009. All rights reserved.
$CVSROOT/userdocs/Examiner_GenPFs.doc (was S.P0468.73.29)
Issue 0.1: (16th October 1995) Initial version
Issue 0.2: (19th October 1995) After initial review
Issue 0.3: (1st November 1995) Conversion to Praxis standard document
Issue 1.0: (22nd November 1995) After formal review
Issue 2.0: (30th June 1997) Conversion to new standard document
Issue 2.9: (27th August 1997) Updating for Examiner Release 3.0, made provisional
Issue 3.0: (2nd September 1997) After formal review
Issue 3.1: (16th December 1997) Minor formatting changes made and document set corrected
Issue 3.2: (5th July 2000) Minor formatting changes and corrections for Release 5.0
Issue 4.0: (10th July 2000) After review
Issue 4.1: (5th July 2001) Minor changes for Release 6.0
Issue 6.0: (10th August 2001) After review
Issue 6.1: (9th June 2003) Conversion to new standard document format.
Issue 7.0: (10th June 2003): Minor updated for release 7.0 following review.
Issue 7.1: (6th August 2003): Minor update after change to PF generation.
Issue 7.2:(23rd November 2004): Changed company name only.
Issue 7.3: (22 November 2005) Line Manager change
Issue 7.4: (29th November 2005) Updated following review S.P0468.79.90
Issue 7.5: (7th January 2009) Factored out contact details.
Issue 7.6: (2nd February 2009): Modify copyright notice.
None.