内容简介：The type Element represents the kind of individual values contained by stack objects. Top is used as the index into the array Values and can be zero. The Values array uses 1 for the lower index bound so when Top is zero the enclosing stack object is logica
1. Introduction
To learn a new programming language, an effective approach is to implement data structures common to computer programming. This is an effective strategy because the problem to be solved is well understood and several different forms of a given data structure are possible: bounded versus unbounded, sequential versus thread-safe, and so on. A clear understanding of the problem allows one to focus on the language details, and the multiple forms likely require a wide range of language features.
Fortunately, when learning SPARK, Ada programmers need not start from scratch. We can begin with an existing, production-ready Ada implementation for a common data structure and make the changes necessary to conform to SPARK. This approach is possible because the fundamental design, based on the principles of software engineering, is the same in both languages. We would have a package exporting a private type, with primitive operations manipulating that type; in other words, an abstract data type (ADT). The type might be limited, and might be tagged, using the same criteria in both languages to decide. Those primitive operations that change state would be procedures, with functions designed to be "pure" and side effects avoided. As a result, the changes need not be fundamental or extensive, although they are important and in some cases subtle.
The chosen Ada component is one that I have had for decades and have used in real-world applications. Specifically, this component defines a sequential, bounded stack ADT. The enclosing package is a generic so that the type of data contained in the stack objects need not be hard-coded. By "sequential" I mean that the code is not thread-safe. By "bounded" I mean that it is backed by an array, which as usual entails a discriminant on the private type to set the upper bound of the internal array component. Client misuse of the Push and Pop routines, e.g., pushing onto a full stack, raises exceptions. As Ada has evolved I have applied new features to make the code more robust, for example the Push and Pop routines use preconditions to prevent callers from misusing the abstraction, raising exceptions from within the preconditions instead of the procedure bodies.
This blog entry describes the transformation of that Ada stack ADT into a completely proven SPARK implementation that relies on static verification instead of run-time enforcement of the abstraction’s semantics. We will prove that there are no reads of unassigned variables, no array indexing errors, no range errors, no numeric overflow errors, no attempts to push onto a full stack, no attempts to pop from an empty stack, that subprogram bodies implement their functional requirements, and so on. As a result, we get a maximally robust implementation of a reusable stack abstraction providing all the facilities required for production use.
The transformation will occur in phases, following the adoption levels described in section 2. Each adoption level introduces more rigor and thus defines a simple, incremental transition approach.
Note that I assume familiarity with Ada, including preconditions and postconditions. Language details can be obtained from the online learning facilities available at https://learn.adacore.com/ , an interactive site allowing one to enter, compile, and execute Ada programs in a web browser. We also assume a degree of familiarity with SPARK. That same web site provides a similar interactive environment and materials for learning SPARK, including formal proof.
2. SPARK Adoption Levels
In 2016, AdaCore collaborated with Thales in a series of experiments on the application of SPARK to existing software projects written in Ada. The resulting document presents a set of guidelines for adopting formal verification in existing projects. These guidelines are arranged in terms of five levels of software assurance, in increasing order of benefits and costs. The levels are named Stone, Bronze, Silver, Gold and Platinum. Successfully reaching a given level requires successfully achieving the goals of the previous levels as well.
The guidelines were developed jointly by AdaCore and Thales for the adoption of the SPARK language technology at Thales but are applicable across a wide range of application domains. The document is available online: http://www.adacore.com/knowled...
2.1 Stone Level
The goal at the Stone level is to identify as much code as possible that belongs to the SPARK subset. That subset provides a strong semantic coding standard that enforces safer use of Ada language features and forbids those features precluding analysis (e.g., exception handlers). The result is potentially more understandable, maintainable code.
2.2 Bronze Level
The goal at the Bronze level is to verify initialization and correct data flow, as indicated by the absence of GNATprove messages during SPARK flow analysis. Flow analysis detects programming errors such as reading uninitialized data, problematic aliasing between formal parameters, and data races between concurrent tasks. In addition, GNATprove checks unit specifications for the actual data read or written, and the flow of information from inputs to outputs. As one can see, this level provides significant benefits, and can be reached with comparatively low cost. There are no proofs attempted at this level, only data and flow analyses.
2.3 Silver Level
The goal at the Silver level is to statically prove absence of run-time errors (AoRTE), i.e., that there are no exceptions raised. Proof at this level detects programming errors such as divide by zero, array indexes that are out of bounds, and numeric overflow (integer, fixed-point and floating-point), among others. These errors are detected via the implicit language-defined checks that raise language-defined exceptions. The checks themselves preclude a number of significant situations, including, for example, buffer overflow, which is often exploited to inject malicious executable code.
Preconditions, among other additions, may be required to prove these checks. To illustrate the benefit and part of the cost of achieving the Silver level, consider the way the Ada version of the stack ADT uses preconditions for this purpose. (The complete Ada implementation is explored in section 4.1.) First, here is the full declaration for type Stack in the Ada package private part:
type Content is array (Positive range <>) of Element; type Stack (Capacity : Positive) is record Values : Content (1 .. Capacity); Top : Natural := 0; end record;
The type Element represents the kind of individual values contained by stack objects. Top is used as the index into the array Values and can be zero. The Values array uses 1 for the lower index bound so when Top is zero the enclosing stack object is logically empty. The following function checks for that condition:
function Empty (This : Stack) return Boolean is (This.Top = 0);
Consider, then, a function using Empty as a precondition. The function takes a stack parameter as input and returns the Element value at the logical top of the stack:
19 function Top_Element (This : Stack) return Element with 20 Pre => not Empty (This);
Given the precondition on line 20, within the function completion we know that Top has a value that is a potentially valid array index. (We'll also have to be more precise about Top's upper bound, as explained later in section 4.4.) There is no need for defensive code so the body is simply as follows:
57 function Top_Element (This : Stack) return Element is 58 (This.Values (This.Top));
If we did not have the precondition specified, GNATprove would issue a message:
58:24: medium: array index check might fail, (e.g. when This = (…, Top => 0) and …)
The message shows an example situation in which the check could fail: Top is zero, i.e., the stack is empty. (We have elided some of the message content to highlight the part mentioning Top.)
GNATprove will attempt to prove, statically, that the preconditions hold at every call site, flagging those calls, if any, in which the preconditions might not hold. Those failures must be addressed at the Silver level because the preconditions are necessary to the proof of absence of run-time errors.
As you can see, the Silver level provides highly significant benefits, but does require more contracts and potentially complex changes to the code. The effort required to achieve this level can be high. Arguably, however, this level should be the minimum target level, especially if the application executable is to be deployed with run-time checks disabled.
2.4 Gold Level
The goal at the Gold level is proof of key integrity properties. These properties are typically derived from software requirements but also include maintaining critical data invariants throughout execution.
Working at this level assumes prior completion at the Silver level to ensure program integrity, such that control flow cannot be circumvented through run-time errors and data cannot be corrupted. Verification at this level is also expected to pass without any violations.
Key integrity properties are expressed as additional preconditions and postconditions beyond those used for defensive purposes. In addition, the application may explicitly raise application-defined exceptions to signal violations of integrity properties. GNATprove will attempt to prove that the code raising an exception is never reached, and thus, that the property violation never occurs. This approach may also require further proof-oriented code.
The Gold level provides extremely significant benefits. In particular, it can be less expensive to prove at this level than to test to the same degree of confidence. However, the analysis may take a long time, may require adding more precise types (ranges), and may require adding more preconditions and postconditions. Even if a property is provable, automatic provers may fail to prove it due to limitations of the provers, requiring either manual proof or, alternatively, testing.
2.5 Platinum Level
The goal at the Platinum level is nothing less than full functional proof of the requirements, including the functional unit level requirements, but also any abstract requirements such as, for example, safety and security.
As with the Gold level, the application code must pass SPARK analysis without any violations. Furthermore, at the Platinum level GNATprove must verify complete user specifications for type invariants, preconditions, postconditions, type predicates, loop variants, and loop termination.
The effort to achieve Platinum level is high, so high that this level is not recommended during initial adoption of SPARK.
3. Development Environment and Configuration
When we say we use SPARK, we mean that we develop the sources in the SPARK language, but also that we use the SPARK analysis tool to examine and verify those sources. We developed our sources in GNAT Studio (formerly GPS), a multi-lingual IDE supporting both Ada and SPARK, among others. The SPARK analysis tool is named GNATprove, a command-line tool integrated with GNAT Studio. GNAT Studio facilitates invocation of GNATprove with control over switches and source files, providing traversable results and even, if need be, interactive proof.
3.1 The Provers
A critical concept for using GNATprove is that it transparently invokes third-party “provers” to analyze the given source files. These provers are somewhat specialized in their ability to analyze specific semantics expressed by the source code. As a result, invocation of a series of provers may be required before some source code is successfully proven. In addition, we may need to ask the provers to “try harder” when attempting to analyze difficult situations. GNATprove can do both for us via the “level=n” switch, where “n” is a number from 0 to 4 indicating increasing strength of analysis and additional provers invoked. In proving our stack implementation we use level 4.
3.2 Language-Defined Run-time Checks
GNATprove is also integrated with the GNAT Ada compiler, including the analysis of language-defined run-time checks produced by the compiler. GNATprove attempts to verify that no exceptions are raised due to these checks. It will do so even if we suppress the checks with compiler switches or pragma Suppress, so we can interpret lack of corresponding messages as successful verification of those checks.
Integer overflow checks are a special case, and as a result have a dedicated GNAT switch that affects whether that specific check is generated by the compiler. They are a special case because, in addition to the functional code, they may appear in the logical assertions about the functional code, including subprogram preconditions and postconditions. In these contexts, we might expect them to behave mathematically, without implementation bounds. For example, consider the following declaration for a procedure that enters a log entry into a file:
5 Entry_Num : Natural := 0; 6 7 procedure Log (This : String) with 8 Pre => Entry_Num + 1 <= Integer'Last, 9 Global => (In_Out => Entry_Num);
The procedure body increments Entry_Num by one and then prepends the result to the string passed as the log entry. This addition in the body might overflow, but the issue under consideration is the addition in the precondition on line 8. If Entry_Num is Integer’Last at the point of the call, the addition on line 8 will overflow, as GNATprove indicates:
8:26: medium: overflow check might fail (e.g. when Entry_Num = Natural'Last)
We could revise the code so that the expression cannot overflow:
Pre => Entry_Num <= Integer'Last - 1,
although that is slightly less readable. Other alternatives within the code are possible as well. However, with regard to switches pertinent for check generation, GNAT provides the “-gnato” switch that allows us to control how integer overflow is treated. (There is a pragma as well, with the same effects.) We can use that switch to have the compiler implement integer arithmetic mathematically, without bounds, the way we might conceptually expect it to work within logical, non-functional assertions. As a result, there will be no integer overflow checks generated. The default effect for the switch, and the default if the switch is not present, is to enable overflow checks in both functional and assertion code so we just need to be aware of non-default usage when we want to determine whether integer overflow checks have been verified. (See the SPARK User Guide, section 5.7 “Overflow Modes” for the switch parameters.) In our GNAT project file, the switch is explicitly set to enable overflow checks in both the functional code and the assertion code.
3.3 Source Code File Organization
The main program declares objects of a type Stack able to contain character values. That Stack type is provided by the package Character_Stacks, which is an instantiation of a generic package defining a stack abstract data type. The instantiation is specified such that objects of the resulting Stack type can contain character values.
Logically, there are four source files in the application: two (declaration and body) for the generic package, one for the instantiation of that generic package, and one containing the demonstration main subprogram. Operationally, however, there are multiple source files for the generic package. Rather than have one implementation that we alter as we progress through the SPARK adoption levels, we have chosen to have a distinct generic package for each level. Each generic package implements a common stack ADT in a manner consistent with an adoption level. The differences among them reflect the changes required for the different levels. This approach makes it easier to keep the differences straight when examining the code. Furthermore, we can apply the proof analyses to a conceptually common abstraction at arbitrary adoption levels without having to alter the code.
In addition to the content differences required by the adoption levels, each generic package name reflects the corresponding level. We have generic package Bounded_Stacks_Stone for the Stone level, Bounded_Stacks_Gold for the Gold level, and so on. Therefore, although the instantiation is always named Character_Stacks, we have multiple generic packages available to declare the one instantiation used.
There are also multiple files for the instantiations. Each instantiation is located within a dedicated source file corresponding to a given adoption level (lines 2 and 3 below). For example, here is the content of the file providing the instance for the Stone level:
1 pragma Spark_Mode (On); 2 with Bounded_Stacks_Stone; 3 package Character_Stacks is new Bounded_Stacks_Stone 4 (…);
The file names for these instances must be unique but are otherwise arbitrary. For the above, the file name is “character_stacks-stone.ads” because it is the instance of the Stone level generic.
Only one of these instances can be used when GNATprove analyzes the code (or when building the executable). To select among them we use a “scenario variable” defined in the GNAT project file that has scenario values matching the adoption level names. In the IDE this scenario variable is presented with a pull-down menu so all we must do to work at a given level is select the adoption level name in the pull-down list. The project file then selects the instantiation file corresponding to the level, e.g., “character_stacks-silver.ads” when the Silver level is selected.
There are also multiple source files for the main program. Rather than have one file that must be edited as we prove the higher levels, we have two: one for all levels up to and including the Silver level, and one for all levels above that. The scenario variable also determines which of these two source files is active.
3.4 Verifying Generic Units
One of the current limitations of GNATprove is that it cannot verify generic units on their own. GNATprove must instead be provided an instantiation to verify. Therefore, whenever we say that we are verifying the generic package defining the stack ADT, we mean we are invoking GNATprove on an instantiation of that generic. As noted earlier in section 3.3, there are multiple source files containing these instantiations so we must select the file corresponding to the desired level when we want to verify the generic package alone.
However, because there are only four total files required at any one time, we usually invoke the IDE action that has GNATprove analyze all the files in the closure of the application. The instantiation file corresponding to the scenario variable’s current selection will be analyzed; other instantiation files are ignored. This approach also verifies the main program’s calls to the stack routines, which is vital to the higher adoption levels.
4. Implementations Per Adoption Level
Our first main procedure, used for all adoption levels up through Silver, declares two stack objects (line 6 below) and manipulates them via the abstraction’s interface:
1 with Ada.Text_IO; use Ada.Text_IO;
2 with Character_Stacks; use Character_Stacks;
3
4 procedure Demo_AoRTE with SPARK_Mode is
5
6 S1, S2 : Stack (Capacity => 10); -- arbitrary
7
8 X, Y : Character;
9
10 begin
11 pragma Assert (Empty (S1) and Empty (S2));
12 pragma Assert (S1 = S2);
13 Push (S1, 'a');
14 Push (S1, 'b');
15 Put_Line ("Top of S1 is '" & Top_Element (S1) & "'");
16
17 Pop (S1, X);
18 Put_Line ("Top of S1 is '" & Top_Element (S1) & "'");
19 Pop (S1, Y);
20 pragma Assert (Empty (S1) and Empty (S2));
21 Put_Line (X & Y);
22
23 Reset (S1);
24 Put_Line ("Extent of S1 is" & Extent (S1)'Image);
25
26 Put_Line ("Done");
27 end Demo_AoRTE;
This is the “demo_aorte.adb” file. The purpose of the code is to illustrate issues found at the initial levels, including proof in a caller context. It has no other functional purpose whatsoever. As we progress through the levels, we will add more assertions to highlight more issues, as will be seen in the other main procedure in the “demo_gold.adb” file.
4.1 Initial Ada Implementation
The initial version defines a canonical representation of a sequential, bounded stack. As an abstract data type, the Stack type is declared as a private type with routines manipulating objects of the type. The type is declared within a generic package that has one generic formal parameter, a type representing the kind of elements contained by Stack objects. This approach is used in all the implementations.
Some routines have “defensive” preconditions to ensure correct functionality. They raise exceptions, declared within the package, when the preconditions do not hold.
The generic package in Ada is declared as follows:
1 generic 2 type Element is private; 3 package Bounded_Stacks_Magma is 4 5 type Stack (Capacity : Positive) is private; 6 7 procedure Push (This : in out Stack; Item : in Element) with 8 Pre => not Full (This) or else raise Overflow; 9 10 procedure Pop (This : in out Stack; Item : out Element) with 11 Pre => not Empty (This) or else raise Underflow; 12 13 function Top_Element (This : Stack) return Element with 14 Pre => not Empty (This) or else raise Underflow; 15 -- Returns the value of the Element at the "top" of This 16 -- stack, i.e., the most recent Element pushed. Does not 17 -- remove that Element or alter the state of This stack 18 -- in any way. 19 20 overriding function "=" (Left, Right : Stack) return Boolean; 21 22 procedure Copy (Destination : out Stack; Source : Stack) with 23 Pre => Destination.Capacity >= Extent (Source) 24 or else raise Overflow; 25 -- An alternative to predefined assignment that does not 26 -- copy all the values unless necessary. It only copies 27 -- the part "logically" contained, so is more efficient 28 -- when Source is not full. 29 30 function Extent (This : Stack) return Natural; 31 -- Returns the number of Element values currently 32 -- contained within This stack. 33 34 function Empty (This : Stack) return Boolean; 35 36 function Full (This : Stack) return Boolean; 37 38 procedure Reset (This : out Stack); 39 40 Overflow : exception; 41 Underflow : exception; 42 43 private 44 45 type Content is array (Positive range <>) of Element; 46 47 type Stack (Capacity : Positive) is record 48 Values : Content (1 .. Capacity); 49 Top : Natural := 0; 50 end record; 51 52 end Bounded_Stacks_Magma;
This version is below the Stone level because it is not within the SPARK subset, due to the raise expressions on lines 8, 11, 14, and 24. We will address those constructs in the Stone version.
The generic package body is shown below.
1 package body Bounded_Stacks_Magma is 2 3 procedure Reset (This : out Stack) is 4 begin 5 This.Top := 0; 6 end Reset; 7 8 function Extent (This : Stack) return Natural is 9 (This.Top); 10 11 function Empty (This : Stack) return Boolean is 12 (This.Top = 0); 13 14 function Full (This : Stack) return Boolean is 15 (This.Top = This.Capacity); 16 17 procedure Push (This : in out Stack; Item : in Element) is 18 begin 19 This.Top := This.Top + 1; 20 This.Values (This.Top) := Item; 21 end Push; 22 23 procedure Pop (This : in out Stack; Item : out Element) is 24 begin 25 Item := This.Values (This.Top); 26 This.Top := This.Top - 1; 27 end Pop; 28 29 function Top_Element (This : Stack) return Element is 30 (This.Values (This.Top)); 31 32 function "=" (Left, Right : Stack) return Boolean is 33 (Left.Top = Right.Top and then 34 Left.Values (1 .. Left.Top) = Right.Values (1 .. Right.Top)); 35 36 procedure Copy (Destination : out Stack; Source : Stack) is 37 subtype Contained is Integer range 1 .. Source.Top; 38 begin 39 Destination.Top := Source.Top; 40 Destination.Values (Contained) := Source.Values (Contained); 41 end Copy; 42 43 end Bounded_Stacks_Magma;
Note that both procedure Copy and function “=” are defined for the sake of increased efficiency when the objects in question are not full. The procedure only copies the slice of Source.Values that represents the Element values logically contained at the time of the call. The language-defined assignment operation, in contrast, would copy the entire contents. Similarly, the overridden equality operator only compares the array slices, rather than the entire arrays, after first ensuring the stacks are the same logical size.
The changes to the body made for the sake of SPARK will amount to moving certain bodies to the package declaration so we will not show the package body again. The full Platinum implementation, both declaration and body, is provided in section 6.
4.2 Stone Implementation
The Stone level version of the package cannot have the "raise expressions" in the preconditions because they are not in the SPARK subset. The rest of the preconditions are unchanged. Here are the updated declarations for Push and Pop, for example:
procedure Push (This : in out Stack; Item : in Element) with
Pre => not Full (This);
procedure Pop (This : in out Stack; Item : out Element) with
Pre => not Empty (This);
When we get to the adoption levels involving proof, GNATprove will attempt to verify statically that the preconditions will hold at each call site. Either that verification will succeed, or we will know that we must change the calling code accordingly. Therefore, the prohibited “raise expressions” are not needed.
The exception declarations, although within the subset, are also removed because they are no longer needed.
The remaining code is wholly within the SPARK subset so we have reached the Stone level.
4.3 Bronze Implementation
The Bronze level is about initialization and data flow. When we apply GNATprove to the Stone version in flow analysis mode, GNATprove issues messages on the declarations of procedures Copy and Reset in the generic package declaration:
medium: "Destination.Values" might not be initialized in "Copy" high: "This.Values" is not initialized in "Reset"
The procedure declarations are repeated below for reference:
procedure Copy (Destination : out Stack; Source : Stack) with
Pre => Destination.Capacity >= Extent (Source);
procedure Reset (This : out Stack);
Both messages result from the fact that the updated formal stack parameters have mode “out” specified. That mode, in SPARK, means more than it does in Ada. It indicates that the actual parameters are fully assigned by the procedures, but these two procedure bodies do not do so. Procedure Reset simply sets the Top to zero because that is all that a stack requires, at run-time, to be fully reset. It does nothing at all to the Values array component. Likewise, procedure Copy may only assign part of the array, i.e., just those array components that are logically part of the Source object. (Of course, if Source is full, the entire array is copied.) In both subprograms our notion of being fully assigned is less than SPARK requires. Therefore, we have two choices. Either we assign values to all components of the record, or we change the modes to “in out.” These two procedures exist for the sake of efficiency, i.e., not writing any more data than logically necessary. Having Reset assign anything to the array component would defeat the purpose. For the same reason, having Copy assign more than the partial slice (when the stack is not full) is clearly inappropriate. Therefore, we change the mode to “in out” for these two subprograms. In other cases we might change the implementations to fully assign the objects.
The other change required for initialization concerns the type Stack itself. In the main subprogram, GNATprove complains that the two objects of type Stack have not been initialized:
warning: "S1" may be referenced before it has a value high: private part of "S1" is not initialized warning: "S2" may be referenced before it has a value high: private part of "S2" is not initialized high: private part of "S1" is not initialized
Our full definition of the Stack type in the private part is such that default initialization (i.e., elaboration of object declarations without an explicit initial value) will assign the record components so that a stack will behave as if initially empty. Specifically, default initialization assigns zero to Top (line 5 below), and since function Empty examines only the Top component, such objects are empty.
1 type Content is array (Positive range <>) of Element; 2 3 type Stack (Capacity : Positive) is record 4 Values : Content (1 .. Capacity); 5 Top : Natural := 0; 6 end record;
Proper run-time functionality of the Stack ADT does not require the Values array component to be assigned by default initialization. But just as with Reset and Copy, although this approach is sufficient at run-time, the resulting objects will not be fully initialized in SPARK, which analyzes the code prior to run-time. As a result, we need to assign an array aggregate to the Values component as well. Expressing the array aggregate is problematic because the array component type is the generic formal private type Element, with a private view within the package. Inside the generic package we don’t know how to construct a value of type Element so we cannot construct an aggregate containing such values. Therefore, we add the Default_Value generic formal object parameter and use it to initialize the array components.
This new generic formal parameter, shown below on line 5, is added from the Bronze version onward:
1 generic 2 type Element is private; 3 -- The type of values contained by objects of type Stack 4 5 Default_Value : Element; 6 -- The default value used for stack contents. Never 7 -- acquired as a value from the API, but required for 8 -- initialization in SPARK. 9 package Bounded_Stacks_Bronze is
The full definition for type Stack then uses that parameter to initialize Values (line 2):
1 type Stack (Capacity : Positive) is record 2 Values : Content (1 .. Capacity) := (others => Default_Value); 3 Top : Natural := 0; 4 end record;
With those changes in place flow analysis completes without further complaint. The implementation has reached the Bronze level.
The need for that additional generic formal parameter is unfortunate because it becomes part of the user’s interface without any functional use. None of the API routines ever return it as such, and the actual value chosen is immaterial.
Note that SPARK will not allow the aggregate to contain default components (line 2):
1 type Stack (Capacity : Positive) is record 2 Values : Content (1 .. Capacity) := (others => <>); 3 Top : Natural := 0; 4 end record;
as per SPARK RM 4.3(1).
Alternatively, we could omit this generic formal object parameter if we use an aspect to promise that the objects are initially empty, and then manually justify any resulting messages. We will in fact add that aspect for other reasons, but we prefer to have proof as automated as possible, for convenience and to avoid human error.
Finally, although the data dependency contracts, i.e., the “Global” aspects, would be generated automatically, we add them explicitly, indicating that there are no intended accesses to any global objects. For example, on line 3 in the following:
1 procedure Push (This : in out Stack; Item : Element) with 2 Pre => not Full (This), 3 Global => null;
We do so because mismatches between reality and the generated contracts are not reported by GNATprove, but we prefer positive confirmation for our understanding of the dependencies.
The flow dependency contracts (the “Depends” aspects) also can be generated automatically. Unlike the data dependency contracts, however, usually these can be omitted from the code even though mismatches with the corresponding bodies are not reported. That lack of notification is not a problem because the generated contracts are safe: they express at least the dependencies that the code actually exhibits. Therefore, all actual dependencies are covered. For example, a generated flow dependency will state that all outputs depend on all inputs, which is possible but not necessarily the case.
However, overly conservative contracts can lead to otherwise-avoidable issues with proof, leading the developer to add precise contracts explicitly when necessary. The other reason to express them explicitly is when we want to prove data flow dependencies as part of the abstract properties, for example data flowing only between units at appropriate security levels. We are not doing so in this case.
4.4 Silver Implementation
If we try to prove the Bronze level version of the generic package, GNATprove will complain about various run-time checks that cannot be proved in the generic package body. The Silver level requires these checks to be proven not to fail, i.e., not to raise exceptions.
The check messages are as follows, preceded by the code fragments they reference, with some message content elided in order to emphasize parts that lead us to the solution:
37 procedure Push (This : in out Stack; Item : in Element) is 38 begin 39 This.Top := This.Top + 1; 40 This.Values (This.Top) := Item; 41 end Push;
bounded_stacks_silver.adb:39:28: medium: overflow check might fail, … (e.g. when This = (…, Top => Natural'Last) … bounded_stacks_silver.adb:40:24: medium: array index check might fail, … (e.g. when This = (…, Top => 2) and This.Values'First = 1 and This.Values'Last = 1)
47 procedure Pop (This : in out Stack; Item : out Element) is 48 begin 49 Item := This.Values (This.Top); 50 This.Top := This.Top - 1; 51 end Pop;
bounded_stacks_silver.adb:49:32: medium: array index check might fail, … (e.g. when This = (…, Top => 2) and This.Values'First = 1 and This.Values'Last = 1)
57 function Top_Element (This : Stack) return Element is 58 (This.Values (This.Top));
bounded_stacks_silver.adb:58:24: medium: array index check might fail, … (e.g. when This = (…, Top => 2) and This.Values'First = 1 and This.Values'Last = 1)
64 function "=" (Left, Right : Stack) return Boolean is 65 (Left.Top = Right.Top and then 66 Left.Values (1 .. Left.Top) = Right.Values (1 .. Right.Top));
bounded_stacks_silver.adb:66:12: medium: range check might fail, … (e.g. when Left = (Capacity => 1, …, Top => 2) … bounded_stacks_silver.adb:66:43: medium: range check might fail, … (e.g. when Right = (Capacity => 1, …, Top => 2) …
72 procedure Copy (Destination : in out Stack; Source : Stack) is 73 subtype Contained is Integer range 1 .. Source.Top; 74 begin 75 Destination.Top := Source.Top; 76 Destination.Values (Contained) := Source.Values (Contained); 77 end Copy;
bounded_stacks_silver.adb:76:47: medium: range check might fail, … (e.g. when Destination = (Capacity => 1, …) and Source = (Capacity => 1, …), Top => 2)
All of these messages indicate that the provers do not know that the Top component is always in the range 0 .. Capacity. The code has not said so, and indeed, there is no way to use a discriminant in a scalar record component declaration to constrain the component’s range. This is what we would write for the record type implementing type Stack in the full view, if we could (line 3):
1 type Stack (Capacity : Positive) is record 2 Values : Content (1 .. Capacity) := (others => Default_Value); 3 Top : Natural range 0 .. Capacity := 0; 4 end record;
but that range constraint on Top is not legal. The reason it is illegal is that the application can change the value of a discriminant at run-time, under controlled circumstances, but there is no way at run-time to change the range checks in the object code generated by the compiler. However, with Ada and SPARK there is now a way to express the constraint on Top, and the provers will recognize the meaning during analysis. Specifically, we apply a “subtype predicate” to the record type declaration (line 5):
1 type Stack (Capacity : Positive) is record 2 Values : Content (1 .. Capacity) := (others => Default_Value); 3 Top : Natural := 0; 4 end record with 5 Predicate => Top in 0 .. Capacity;
This aspect informs the provers that the Top component for any object of type Stack is always in the range 0 .. Capacity. That addition successfully addresses all the messages about the generic package body. Note that the provers will verify the predicate too.
However, GNATprove also complains about the main program. Consider that the first two assertions in the main procedure are not verified:
10 begin 11 pragma Assert (Empty (S1) and Empty (S2)); 12 pragma Assert (S1 = S2);
GNATprove emits:
11:19: medium: assertion might fail, cannot prove Empty (S1) 12:19: medium: assertion might fail, cannot prove S1 = S2
We can address the issue for function Empty, partly, by adding another aspect to the declaration of type Stack, this time to the visible declaration:
type Stack (Capacity : Positive) is private
with Default_Initial_Condition => Empty (Stack);
The new aspect indicates that default initialization results in stack objects that are empty, making explicit, and especially, verifiable, the intended initial object state. We will be notified if GNATprove determines that the aspect does not hold.
That new aspect will handle the first assertion in the main program on line 11 but GNATprove complains throughout the main procedure that the preconditions involving Empty and Full cannot be proven. For example:
13 Push (S1, 'a');
14 Push (S1, 'b');
15 Put_Line ("Top of S1 is '" & Top_Element (S1) & "'");
GNATprove emits:
13:06: medium: precondition might fail, cannot prove not Full (This) 14:06: medium: precondition might fail, cannot prove not Full (This) [possible explanation: call at line 13 should mention This (for argument S1) in a postcondition] 15:35: medium: precondition might fail, cannot prove not Empty (This) [possible explanation: call at line 14 should mention This (for argument S1) in a postcondition]
Note the “possible explanations” that GNATprove gives us. These are clear indications that we are not specifying sufficient postconditions. Remember that when analyzing code that includes a call to some procedure, the provers’ knowledge of the call’s effect is provided entirely by the procedure’s postcondition. That postcondition might be insufficient, especially if it is absent!
Therefore, we must tell the provers about the effects of calling Push and Pop, as well as the other routines that change state. We add a new postcondition on Push (line 3):
1 procedure Push (This : in out Stack; Item : Element) with 2 Pre => not Full (This), 3 Post => Extent (This) = Extent (This)'Old + 1, 4 Global => null;
The new postcondition expresses the fact that the Stack contains one more Element value after the call. This is sufficient because the provers know that function Extent is simply the value of Top:
function Extent (This : Stack) return Natural is
(This.Top);
Hence the provers know that Top is incremented by Push.
The same approach addresses the messages for Pop (line 3):
1 procedure Pop (This : in out Stack; Item : out Element) with 2 Pre => not Empty (This), 3 Post => Extent (This) = Extent (This)'Old - 1, 4 Global => null;
In the above we say that the provers know what the function Extent means. For that to be the case when verifying client calls, we must move the function completion from the generic package body to the generic package declaration. In addition, the function must be implemented as an “expression function,” which Extent already is (see above). As expression functions in the package spec, the provers will know the semantics of those functions automatically, as if each is given a postcondition restating the corresponding expression explicitly. We also need functions Full and Empty to be known in this manner. Therefore, we move the Extent, Empty, and Full function completions, already expression functions, from the generic package body to the package declaration. We put them in the private part because these implementation details should not be exported to clients.
However, we have a potential overflow in the postcondition for Push, i.e., the increment of the number of elements contained after Push returns (line 3 below). The postcondition for procedure Pop, of course, does not have that problem.
1 procedure Push (This : in out Stack; Item : Element) with 2 Pre => not Full (This), 3 Post => Extent (This) = Extent (This)'Old + 1, 4 Global => null;
The increment might overflow because Extent returns a value of subtype Natural, which could be the value Integer'Last. Hence the increment could raise Constraint_Error and the check cannot be verified. We must either apply the “-gnato” switch so that assertions can never overflow, or alternatively, declare a safe subrange so that the result of the addition cannot be greater than Integer'Last.
Our choice is to declare a safe subrange because the effects are explicit in the code, as opposed to an external switch. Here are the added subtype declarations:
subtype Element_Count is
Integer range 0 .. Integer'Last - 1;
-- The number of Element values currently contained
-- within any given stack. The lower bound is zero
-- because a stack can be empty. We limit the upper
-- bound (minimally) to preclude overflow issues.
subtype Physical_Capacity is
Element_Count range 1 .. Element_Count'Last;
-- The range of values that any given stack object can
-- specify (via the discriminant) for the number of
-- Element values the object can physically contain.
-- Must be at least one.
We use the second subtype for the discriminant in the partial view for Stack (line 1):
1 type Stack (Capacity : Physical_Capacity) is private 2 with Default_Initial_Condition => Empty (Stack);
and both subtypes in the full declaration in the private part (lines 1, 3, and 5):
1 type Content is array (Physical_Capacity range <>) of Element; 2 3 type Stack (Capacity : Physical_Capacity) is record 4 Values : Content (1 .. Capacity) := (others => Default_Value); 5 Top : Element_Count := 0; 6 end record with 7 Predicate => Top in 0 .. Capacity;
The function Extent is changed to return a value of the subtype Element_Count so adding one in the postcondition cannot go past Integer’Last. Overflow is precluded but note that there will now be range checks for GNATprove to verify.
With these changes in place we have achieved the Silver level. There are no run-time check verification failures and the defensive preconditions are proven at their call sites.
4.5 Gold Implementation
We will now address the remaining changes needed to reach the Gold level. The process involves iteratively attempting to prove the main program that calls the stack routines and makes assertions about the conditions that follow. This process will result in changes to the generic package, especially postconditions, so it will require verification along with the main procedure. Those additional postconditions may require additional preconditions as well.
In general, a good way to identify postcondition candidates is to ask ourselves what conditions we, as the developers, know to be true after a call to the routine in question. Then we can add assertions after the calls to see if the provers can verify those conditions. If not, we extend the postcondition on the routine.
For example, we can say that after a call to Push, the corresponding stack cannot be empty. Likewise, after a call to Pop, the stack cannot be full. These additions are not required for the sake of assertions or other preconditions because the Extent function already tells the provers what they need to know in this regard. However, they are good documentation and may be required to prove additional conditions added later. (That is the case, in fact, as will be shown.)
To see what other postconditions are required, we now switch to the other main procedure, in the “demo_gold.adb” file. This version of the demo program includes a number of additional assertions:
1 with Ada.Text_IO; use Ada.Text_IO;
2 with Character_Stacks; use Character_Stacks;
3
4 procedure Demo_Gold with SPARK_Mode is
5
6 S1, S2 : Stack (Capacity => 10); -- arbitrary
7
8 X, Y : Character;
9
10 begin
11 pragma Assert (Empty (S1) and Empty (S2));
12 pragma Assert (S1 = S2);
13 Push (S1, 'a');
14 pragma Assert (not Empty (S1));
15 pragma Assert (Top_Element (S1) = 'a');
16 Push (S1, 'b');
17 pragma Assert (S1 /= S2);
18
19 Put_Line ("Top of S1 is '" & Top_Element (S1) & "'");
20
21 Pop (S1, X);
22 Put_Line ("Top of S1 is '" & Top_Element (S1) & "'");
23 Pop (S1, Y);
24 pragma Assert (X = 'b');
25 pragma Assert (Y = 'a');
26 pragma Assert (S1 = S2);
27 Put_Line (X & Y);
28
29 Push (S1, 'a');
30 Copy (Source => S1, Destination => S2);
31 pragma Assert (S1 = S2);
32 pragma Assert (Top_Element (S1) = Top_Element (S2));
33 pragma Assert (Extent (S1) = Extent (S2));
34
35 Reset (S1);
36 pragma Assert (Empty (S1));
37 pragma Assert (S1 /= S2);
38
39 Put_Line ("Done");
40 end Demo_Gold;
For example, we have added assertions after the calls to Reset and Copy, on lines 31 through 33 and 36 through 37, respectively. GNATprove now emits the following (elided) messages for those assertions:
demo_gold.adb:31:19: medium: assertion might fail, cannot prove S1 = S2 (e.g. when S1 = (…, Top => 0) and S2 = (…, Top => 0)) [possible explanation: call at line 30 should mention Destination (for argument S2) in a postcondition]
demo_gold.adb:36:19: medium: assertion might fail, cannot prove Empty (S1) … [possible explanation: call at line 35 should mention This (for argument S1) in a postcondition]
Note again the “possible explanation” hints. For the first message we need to add a postcondition on Copy specifying that the value of the argument passed to Destination will be equal to that of the Source parameter (line 3):
1 procedure Copy (Destination : in out Stack; Source : Stack) with 2 Pre => Destination.Capacity >= Extent (Source), 3 Post => Destination = Source, 4 Global => null;
We must move the “=” function implementation to the package spec so that the provers will know the meaning. The function was already completed as an expression function so moving it to the spec is all that is required.
For the second message, regarding the failure to prove that a stack is Empty after Reset, we add a postcondition to that effect (line 2):
1 procedure Reset (This : in out Stack) with 2 Post => Empty (This), 3 Global => null;
The completion for function Empty was already moved to the package spec, earlier.
The implementations of procedure Copy and function “=” might have required explicit loops, likely requiring loop invariants, but using array slicing we can express the loop implicitly. Here is function “=” again, for example:
1 function "=" (Left, Right : Stack) return Boolean is 2 (Left.Top = Right.Top and then 3 Left.Values (1 .. Left.Top) = Right.Values (1 .. Right.Top));
The slice comparison on line 3 expresses an implicit loop for us, as does the slice assignment in procedure Copy.
The function could have been implemented as follows, with an explicit loop:
1 function "=" (Left, Right : Stack) return Boolean is 2 begin 3 if Left.Top /= Right.Top then 4 -- They hold a different number of element values so 5 -- cannot be equal. 6 return False; 7 end if; 8 -- The two Top values are the same, and the arrays 9 -- are 1-based, so the bounds are the same. Hence the 10 -- choice of Left.Top or Right.Top is arbitrary and 11 -- there is no need for index offsets. 12 for K in 1 .. Left.Top loop 13 if Left.Values (K) /= Right.Values (K) then 14 return False; 15 end if; 16 pragma Loop_Invariant 17 (Left.Values (1 .. K) = Right.Values (1 .. K)); 18 end loop; 19 -- We didn't find a difference 20 return True; 21 end "=";
Note the loop invariant on lines 16 and 17. In some circumstances GNATprove will handle the invariants for us but often it cannot. In practice, writing sufficient loop invariants is one of the more difficult facets of SPARK development so the chance to avoid them is welcome.
Continuing, we know that after the body of Push executes, the top element contained in the stack will be the value passed to Push as an argument. But the provers cannot verify an assertion to that effect (line 15 below):
13 Push (S1, 'a'); 14 pragma Assert (not Empty (S1)); 15 pragma Assert (Top_Element (S1) = 'a');
GNATprove emits this message:
demo_gold.adb:15:19: medium: assertion might fail, cannot prove Top_Element (S1) = 'a'
We must extend the postcondition for Push to state that Top_Element would return the value just pushed, as shown on line 4 below:
1 procedure Push (This : in out Stack; Item : Element) with 2 Pre => not Full (This), 3 Post => not Empty (This) 4 and then Top_Element (This) = Item 5 and then Extent (This) = Extent (This)'Old + 1, 6 Global => null;
Now the assertion on line 15 is verified successfully.
Recall that the precondition for function Top_Element is that the stack is not empty. We already have that assertion in the postcondition (line 3) so the precondition for Top_Element is satisfied. We must use the short circuit form for the conjunction, though, to control the order of evaluation so that “not Empty” is verified before Top_Element.
The short-circuit form on line 4 necessitates the same form on line 5, per Ada rules. That triggers a subtle issue flagged by GNATprove. The short-circuit form, by definition, means that the evaluation of line 5 might not occur. If it is not evaluated, we’ve told the compiler to call Extent and make a copy of the result (via ‘Old, on the right-hand side of “=”) that will not be needed. Moreover, the execution of Extent might raise an exception. Therefore, the language disallows applying ‘Old in any potentially unevaluated expression that might raise exceptions. As a consequence, in line 5 we cannot apply ‘Old to the result of calling Extent. GNATprove issues this error message:
prefix of attribute "Old" that is potentially unevaluated must denote an entity
We could address the error by changing line 5 to use Extent(This'Old) instead, but there is a potential performance difference between Extent(This)'Old and Extent(This'Old). With the former, only the result of the function call is copied, whereas with the latter, the value of the parameter is copied. Copying the parameter could take significant time and space if This is a large object. Of course, if the function returns a large value the copy will be large too, but in this case Extent only returns an integer.
In SPARK, unlike Ada, preconditions, postconditions, and assertions in general are verified statically, prior to execution, so there is no performance issue. Ultimately, though, the application will be executed. Having statically proven the preconditions and postconditions successfully, we can safely deploy the final executable without them enabled, but not all projects follow that approach (at least, not on that basis). Therefore, for the sake of emphasizing the idiom with typically better performance, we prefer applying ‘Old to the function in our implementation.
We can tell GNATprove that this is a benign case, using a pragma in the package spec:
pragma Unevaluated_Use_of_Old (Allow);
GNATprove will then allow use of ‘Old on the call to function Extent and will ensure that no exceptions will be raised by the function.
As with procedure Push, we can also use Top_Element to strengthen the postcondition for procedure Pop (line 4 below):
1 procedure Pop (This : in out Stack; Item : out Element) with 2 Pre => not Empty (This), 3 Post => not Full (This) 4 and Item = Top_Element (This)'Old 5 and Extent (This) = Extent (This)'Old – 1, 6 Global => null;
Line 4 states that the Item returned in the parameter to Pop is the value that would be returned by Top_Element prior to the call to Pop.
One last significant enhancement now remains to be made. Consider the assertions in the main procedure about the effects of Pop on lines 24 and 25, repeated below:
21 Pop (S1, X);
22 Put_Line ("Top of S1 is '" & Top_Element (S1) & "'");
23 Pop (S1, Y);
24 pragma Assert (X = 'b');
25 pragma Assert (Y = 'a');
Previous lines had pushed ‘a’ and then ‘b’ in that order onto S1. GNATprove emits this one message:
25:19: medium: assertion might fail, cannot prove Y = 'a' (e.g. when Y = 'b')
The message is about the assertion on line 25, alone. The assertion on line 24 was verified. Also, the message indicates that Y could be some arbitrary character. We can conclude that the provers do not know enough about the state of the stack after a call to Pop. The postcondition requires strengthening.
The necessary postcondition extension reflects a unit-level functional requirement for both Push and Pop. If one considers that postconditions correspond to the low-level unit functional requirements (if not more), one can see why the postconditions must be complete. Identifying and expressing complete functional requirements is difficult in itself, and indeed the need for this additional postcondition content is not obvious at first.
The unit-level requirement for both operations is that the prior array components within the stack are not altered, other than the one added or removed. We need to state that Push and Pop have not reordered them, for example. Specifically, for Push we need to say that the new stack state has exactly the same prior array slice contents, ignoring the newly pushed value. For Pop, we need to say that the new state has exactly the prior array slice contents without the old value at the top.
A new function can be used to express these requirements for both Push and Pop:
function Unchanged (Invariant_Part, Within : Stack) return Boolean;
The Within parameter is a stack whose internal state will be compared against that of the Invariant_Part parameter. The name “Invariant_Part” is chosen to indicate the stack state that has not changed. The name "Within" is chosen for readability in named parameter associations on the calls. For example:
Unchanged (X, Within => Y)
means that the Element values of X should be equal to precisely the corresponding values within Y.
However, this function is not one that users would call directly. We only need it for proof. Therefore, we mark the Unchanged function as a "ghost" function so that the compiler will neither generate code for it nor allow the application code to call it. The function is declared with that aspect (on line 2) as follows:
1 function Unchanged (Invariant_Part, Within : Stack) return Boolean 2 with Ghost;
Key to the usage is the fact that by passing This'Old and This to the two parameters we can compare the before/after states of a single object. Viewing the function's implementation will help understand its use in the postconditions:
1 function Unchanged (Invariant_Part, Within : Stack) return Boolean is 2 (Invariant_Part.Top <= Within.Top and then 3 (for all K in 1 .. Invariant_Part.Top => 4 Within.Values (K) = Invariant_Part.Values (K)));
This approach is based directly on a very clever one by Rod Chapman, as seen in some similar code.
The function states that the array components logically contained in Invariant_Part must have the same values as those corresponding array components in Within. Note how we allow Invariant_Part to contain fewer values than the other stack (line 2 above). That is necessary because we use this function in the postconditions for both the Push and Pop operations, in which one more or one less Element value will be present, respectively.
For Push, we add a call to the function in the postcondition as line 6, below:
1 procedure Push (This : in out Stack; Item : Element) with 2 Pre => not Full (This), 3 Post => not Empty (This) 4 and then Top_Element (This) = Item 5 and then Extent (This) = Extent (This)'Old + 1 6 and then Unchanged (This'Old, Within => This), 7 Global => null;
This'Old provides the value of the stack prior to the call of Push, without the new value included, whereas This represents the stack state after Push returns, with the new value in place. Thus, the prior values are compared to the corresponding values in the new state, with the newly included value ignored.
Likewise, we add the function call to the postcondition for Pop, also line 6, below:
以上就是本文的全部内容，希望本文的内容对大家的学习或者工作能带来一定的帮助，也希望大家多多支持 码农网
猜你喜欢:
本站部分资源来源于网络，本站转载出于传递更多信息之目的，版权归原作者或者来源机构所有，如转载稿涉及版权问题，请联系我们。
Database Design and Implementation
Edward Sciore / Wiley / 2008-10-24 / 1261.00 元
* Covering the traditional database system concepts from a systems perspective, this book addresses the functionality that database systems provide as well as what algorithms and design decisions will......一起来看看 《Database Design and Implementation》 这本书的介绍吧!
