程序代写 SWEN90010 – High Integrity

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