SWEN90010 – High Integrity
Systems Engineering Advanced Specification: Ghost Code
Copyright By PowCoder代写 加微信 powcoder
DMD 8.17 (Level 8, Doug McDonell Bldg)
http://people.eng.unimelb.edu.au/tobym @tobycmurray
Ghost Code: additional code whose only purpose is to help prove the original program correct
Can be used only in specifications, i.e. in pre/ postconditions, loop invariants, Assert pragmas, etc.
Common uses:
to express properties you want to prove or assume
to keep track of information in your program that your specifications need to talk about (e.g. history, results of intermediate computations)
A prime candidate that we have already seen
Prevents Storage from being called in real code (it was never meant to be, anyway)
EXAMPLE 2: MATHEMATICAL INTEGERS
A trivial package
6 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
How should “Add” behave?
Add should behave like addition on mathematical integers whenever overflow doesn’t occur
Add(x,y) should give the mathematical x + y whenever the mathematical value of x + y is between Integer’First and Integer’Last (inclusive)
What is wrong with this specification?
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Mathematical Integers in SPARK Ada
Not directly supported in GNAT Prover before 2020
Can be used as Ghost Code in GNAT 2019 via a custom library (https://github.com/joffreyhuguet/curve25519- spark2014)
The package is called Big_Integers
type is called Big_Integer
Need to explicitly convert between Integer types and Big_Integers
(To_Big_Integer, To_Integer, etc.)
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
The “Add” specification
In_Range(A,L,H) abbreviates L <= A and A <= H
Postcondition: convert X to a mathematical integer; do
likewise for Y. Add them together (mathematical
addition). Then the result of Add(X,Y) is equal to that
integer (converted back to a fixed-with machine integer)
9 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
EXAMPLE 3: SUMMING AN ARRAY
Summing an Integer Array
Assume we blindly sum from left to right on a 32-bit machine
Summing these elements will overflow on a 32-bit machine
11 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Specifying Absence of Overflow
How should Sum_Blind behave?
Assuming absence of overflow throughout the entire summation, it should behave like mathematical summation
Requires talking about absence of overflow at all
intermediate points of the computation
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Specifying Absence of Overflow
Solution: build a ghost array of mathematical integers that are the partial sums
Precondition: all values in Sum_Acc are between Integer’First and Integer’Last
Postcondition: The answer is equal to the final value in
Sum_Acc, i.e. to Sum_Acc(Sum_Acc’Last) 13 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
23+-5+ 1021
23+-5+ 1021+ 231-1
Specifying Absence of Overflow
Solution: we write a ghost function to compute the array of partial sums
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com