SWEN90010 – High Integrity
Systems Engineering Safe Language Subsets, SPARK Ada
Copyright By PowCoder代写 加微信 powcoder
DMD 8.17 (Level 8, Doug McDonell Bldg)
http://people.eng.unimelb.edu.au/tobym @tobycmurray
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
What’s wrong with this code?
int binarySearch(int [] list, int target) { int low = 0;
int high = len(list) – 1; int mid;
while(low <= high) {
mid = (low + high)/2;
if (list[mid] < target) {
low = mid + 1;
} else if (list[mid] > target) {
high = mid – 1;
} else {
return mid;
}
return -1;
}
SAFE LANGUAGE SUBSETS
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Safe Languages
Which is safer?
What might make a programming language “safe”?
Predictability: when programs behave as the programmer intended
Implies Verifiability
Doesn’t always mean that the program won’t crash.
Does mean that safe languages are simpler than unsafe ones.
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Design Space
Clean Slate: Design a new, safe programming language e.g. Subset: use an existing language, without all of its unsafe bits.
e.g. SPARK Ada, MISRA C
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Safe Subsets
Removes unsafe parts from a language.
Philosophy: Make programmer work harder
in exchange for much simpler testing and verification.
Advantages
Programs in a safe subset can be compiled and debugged using existing toolchains.
Programmers don’t need to learn a new programming language.
Resulting programs far more tractable to automatically analyse and verify.
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
NASA’s Subset of C
A subset of MISRA C (itself a C subset)
1. Language Compliance
(a) Do not stray outside the language definition.
(b) Compile with all warnings enabled; use static source code analysers.
2. Predictable Execution
(a) Use verifiable loop bounds for all loops meant to be terminating. (b) Do not use direct or indirect recursion.
(c) Do not use dynamic memory allocation after task initialisation. (d) Use IPC messages for task communication.
(e) Do not use task delays for task synchronisation.
(f) Explicitly transfer write-permission (ownership) for shared data objects. (g) Place restrictions on the use of semaphores and locks.
(h) Use memory protection, safety margins, barrier patterns.
(i) Do not use goto, setjmp or longjmp.
(j) Do not use selective value assignments to elements of an enum list.
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
NASA’s Subset of C
A subset of MISRA C (itself a C subset)
3. Defensive Coding
(a) Declare data objects at smallest possible level of scope.
(b) Check the return value of non-void functions, or explicitly cast to (void).
(c) Check the validity of values passed to functions.
(d) Use static and dynamic assertions as sanity checks.
(e) Use U32, I16, etc instead of predefined C data types such as int, short, etc. (f) Make the order of evaluation in compound expressions explicit.
(g) Do not use expressions with side effects.
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
NASA’s Subset of C
A subset of MISRA C (itself a C subset)
4. Code Clarity
(a) Make only very limited use of the C pre-processor.
(b) Do not define macros within a function or a block.
(c) Do not undefine or redefine macros.
(d) Place #else, #elif, and #endif in the same file as the matching #if or #ifdef. (e) Place no more than one statement or declaration per line of text.
(f) Use short functions with a limited number of parameters.
(g) Use no more than two levels of indirection per declaration.
(h) Use no more than two levels of dereferencing per object reference. (i) Do not hide dereference operations inside macros or typedefs.
(j) Do not use non-constant function pointers.
(k) Do not cast function pointers into other types.
(l) Do not place code or declarations before an #include directive.
Maximise: portability, predictability, simplicity.
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
On Simplicity
“There are two ways of constructing a software design. One way is to make it so simple that there are obviously no deficiencies. And the other is to make it so complicated that there are no obvious deficiencies.”
(ACM Turing Award Lecture, 1980)
Start with Ada (already pretty safe language)
Dynamic Memory Allocation Tasks (but see Ravenscar Profile) Goto
Access Types (pointers) Side-effectful expressions and functions
Exception Handling
Add: Annotations
11 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
SPARK Examiner
Checks for conformance to SPARK restrictions
unused assignments,
uses of uninitialised data,
missing return statements
violations of flow contracts (“Depends”)
12 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
SPARKK Prover
Checks for conformance to SPARK restrictions
Plus: uses of uninitialised data,
possible run-time errors, and
functional contracts (“Pre/Post” conditions)
13 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
SPARK Annotations
Mostly By Demonstration
14 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com