1 2 3 4 5 6 7 8 9
1 2 3 4 5 6
The proof is failing because the line:
Result := Input * 10;
Copyright By PowCoder代写 加微信 powcoder
can produce an integer overflow. That is, if Input * 10 is greater than Integer’Last, then the com- putation will give an unexpected value.
If we uncomment the commented lines, the constraint that cannot be proved refers not to the line above, but to the conditions in the branch:
SWEN90010: HIGH INTEGRITY SYSTEMS ENGINEERING DEPARTMENT OF COMPUTING AND INFORMATION SYSTEMS THE UNIVERSITY OF MELBOURNE
Workshop SPARK #1 sample solutions
if Input * 10 <= Integer’Last and
Input * 10 >= Integer’First then
Again, the problem is that Input * 10 could overflow. Although this is not assigned to a variable, our underlying architecture still only handles integers of a certain size. To check that the computation will not overflow, we instead have to switch around the computation to use division instead of multiplication:
procedure Task3Procedure(Input : in Integer; Result : out Integer) is
if Input <= Integer’Last / 10 and
Input >= Integer’First / 10 then
Result := Input * 10;
Fortask4.adb,theproblemagainrelatestoanoverflow:inthiscase,thattheexpressionAnArray(AnIndex) + 1willoverflowifAnArray(AnIndex)isequaltoInteger’Last.
To correct this, we insert a new guard:
procedure Task4Procedure(AnArray : in out MyArray; AnIndex : in Index) is
What this means is that, using the SPARK tools, if all of the conjectures are successfully proved, then we have no integer overflows in our program — a very useful (and sometimes imperative!) property.
For the expression AnArray(AnIndex + 1), the problem is different. This error here relates to that fact that the array could be indexed out of bounds. That is, if AnIndex is equal to Index’Last, then the expressionAnArray(AnIndex + 1)willindexthearrayoutofbounds.Thus,theSPARKtoolsetcould not prove that an out-of-bounds index error was not possible. We can use much the same solution as above to eliminate this:
Result := Input;
end Task3Procedure;
if AnArray(AnIndex) < Integer’Last then
AnArray(AnIndex) := AnArray(AnIndex) + 1;
end Task4Procedure;
if AnIndex < Index’Last then
What this means is that, using the SPARK tools, if all of the conjectures are successfully proved, then we have no index out of bounds errors in our program. A very powerful property – and one that is difficult to detect with tests alone.
For Task1, various issues were detected including uninitialised variables and unassigned variables, plus unused assignment statements. Each of these relates to data flow anomalies. Recalling from SWEN90006:
• A u-r anomaly occurs when an undefined variable is referenced. The reference to the Ok variable in the if-statement is an example. So is the use of I and J when Ok is false.
• A d-u anomaly occurs when a defined variable has not been referenced before it becomes undefined. We did not see any examples of this in Task1 but it is easy to create them.
• A d-d anomaly indicates that the same variable is defined twice causing a hole in the scope of the first definition of the variable. An ineffective assignment statement is an example of this kind of anomaly that we saw in Task1.
For Task3 the type of error was integer overflow (which also includes integer underflow).
For Task4 there were two kinds of overflow: an integer overflow for the values stored in the array, and a possible overflow for the array index (which in other programming languages could lead to a buffer overflow; although such errors cannot occur in Ada which is memory safe).
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com