SPARK
If you know what type-checking and APIs are, skip to the next section.
For those not well-versed in programming language technology I should begin by explaining what static checking means. The most common forms are syntax and type checking. Syntax is simple enough. You just make sure the code is legitimate way of ordering words and symbols. In Java "7++" is not valid but "seven++" is valid if seven is an integer variable. Maybe I shouldn't have said that this was simple? It's just very obvious when you've been doing a lot of programming.
Type checking is slightly more advanced. Every variable and constant has some type. So the aforementioned variable "seven" should be an Integer. If we try to assign the value "3.5" to our variable "seven", we're doing something wrong. The type-checker in Java catches this and tells us we are mixing things up.
This annoys people new to programming because they don't think they should have to declare ahead of time exactly what type a variable has. They're right: a computer can figure this stuff out for itself. Popular languages like Python and Ruby have no type checking. But what they can't do is find a reasonable course of action when I've put a string in a variable used to store numbers, and now try to perform an arithmetic operation on that variable. What does it mean to divide the string "hello world" by 3.2? It doesn't mean anything. It's jibberish and the execution halts.
So type-checking is a way for programmers to catch mistakes before they cause a system to crash during execution. I like type-checking not just because it helps me spot bugs but also because it makes it more clear what kind of value goes where. Programming Python is a pain when you are trying to use libraries that have defined operations like add_time(time_value). What kind of "time_value"? Is there some Time type? Maybe it's a Date? Or DateTime? Types are not absent in Python but they are hidden that makes programming more a matter of trial-and-error than reading the API(documentation).
SPARK Ada
SPARK is a subset of Ada with annotations thrown in. It includes static checking that demands that you declare precisely what it is your trying to do and kicks you if you don't do it. Saying you need a variable X and not using it? SPARK will kick you. Want to access a global variable? You must then declare what variable you want to access and by what criteria you want to modify it. It can be frustrating but I'm dazzled by it. I'm just now getting the hang of it. There are few tutorials so I'll make one of my own.
--------------------------------
package Demo is
procedure Inc(int_val : in out Integer);
--# derives int_val from int_val;
--# pre int_val < Integer'Last;
--# post int_val = int_val~ + 1;
end Demo;
--------------------------------
It turns out the precondition and postcondition are not necessary at this stage. The derivation is. The following is a specification of a package with a single procedure that increments an integer variable.
This states that the value of int_val influences the final value of int_val.
--# derives int_val from int_val;
This states that we only accept int_val that is less than the highest integer number. Otherwise we can't increment it.
--# pre int_val < Integer'Last;
Here we state that int_val ends up being one(1) higher than the initial value.
--# post int_val = int_val~ + 1;
Here is an implementation
--------------------------------
package body Demo is
procedure Inc(int_val : in out Integer) is
begin
int_val := int_val + 1;
end;
end Demo;
--------------------------------
To generate ancillary files
sparkmake
mv spark.idx demo.idx
spark -i=demo.idx -vcg demo.adb
less demo/inc.vcg
The following is the interesting contents of demo/inc.vcg, containing verification conditions:
---------------------------------
For path(s) from start to run-time check associated with statement of line 6:
procedure_inc_1.
H1: int_val < integer__last .
H2: int_val >= integer__first .
H3: int_val <= integer__last .
->
C1: int_val + 1 >= integer__first .
C2: int_val + 1 <= integer__last .
For path(s) from start to finish:
procedure_inc_2.
H1: int_val < integer__last .
H2: int_val >= integer__first .
H3: int_val <= integer__last .
H4: int_val + 1 >= integer__first .
H5: int_val + 1 <= integer__last .
->
C1: int_val + 1 = int_val + 1 .
---------------------------------
These two conclusions of course are quite pointless by themselves. The first conclusion is that "int_val + 1" is greater than or equal to the lowest integer Ada can represent and less than or equal to the highest integer Ada can support. Indeed this is true, though we can refine it further because int_val can not be integer__first. int_val can be, but not int_val + 1. I think I need to modify the precondition!
Hmm, I changed the precondition to
--# pre int_val >= Integer'First and int_val < Integer'Last;
and reran spark -i=demo.idx -vcg but the conclusions are still weak.
I changed the implementation by adding an assertion:
---------------------------------
package body Demo is
procedure Inc(int_val : in out Integer) is
begin
int_val := int_val + 1;
--# assert int_val > Integer'First;
end Inc;
end Demo;
---------------------------------
The new demo.vcg is
---------------------------------
For path(s) from start to run-time check associated with statement of line 6:
procedure_inc_1.
H1: int_val >= integer__first .
H2: int_val < integer__last .
H3: int_val >= integer__first .
H4: int_val <= integer__last .
->
C1: int_val + 1 >= integer__first .
C2: int_val + 1 <= integer__last .
For path(s) from start to assertion of line 7:
procedure_inc_2.
H1: int_val >= integer__first .
H2: int_val < integer__last .
H3: int_val >= integer__first .
H4: int_val <= integer__last .
H5: int_val + 1 >= integer__first .
H6: int_val + 1 <= integer__last .
->
C1: int_val + 1 > integer__first .
C2: int_val + 1 >= integer__first .
C3: int_val + 1 <= integer__last .
C4: int_val >= integer__first .
C5: int_val < integer__last .
For path(s) from assertion of line 7 to finish:
procedure_inc_3.
H1: int_val > integer__first .
H2: int_val >= integer__first .
H3: int_val <= integer__last .
H4: int_val~ >= integer__first .
H5: int_val~ < integer__last .
->
C1: int_val = int_val~ + 1 .
---------------------------------------
So we see that our assertion that int_val is incremented by one at the end of Inc is correct. We also see that the Simplifier doesn't simplify in an optimal way. In procedure_inc_3 the two hypotheses H1 and H2 are equivalent to H1 alone. If int_val must be greater than integer__first then eventuality in the the second hypothesis where int_val = integer__first can never occur. Now I'm intrigued... Maybe I should read more about the rlu-files? They contain additional rules that you can give the prover to help it out. No, I don't need that right now. I'll hold off on rlu-files until the lack of refinement in hypotheses cause a problem.
Let's add a Divide function, to spice things up a bit.
---------------------------------------
package Demo is
procedure Inc(int_val : in out Integer);
--# derives int_val from int_val;
--# pre int_val >= Integer'First and int_val < Integer'Last;
--# post int_val = int_val~ + 1;
function Divide(numerator, denominator : Integer) return Integer;
--# return numerator/denominator;
end Demo;
---------------------------------------
With the following implementation
---------------------------------------
package body Demo is
procedure Inc(int_val : in out Integer) is
begin
int_val := int_val + 1;
--# assert int_val > Integer'First;
end Inc;
function Divide(numerator, denominator : Integer) return Integer is
begin
return numerator/denominator;
end Divide;
end Demo;
---------------------------------------
I can generate VCs for this but no assertions hold for Divide and the last assertion in Inc can no longer be proven. Again, fascinating! Oh, no this isn't right at all...
OK, so now I've straightened things out. Let's start again:
---------------------------------------
package Demo is
procedure Inc(int_val : in out Integer);
--# derives int_val from int_val;
--# pre int_val >= Integer'First and int_val < Integer'Last;
--# post int_val = int_val~ + 1;
end Demo;
---------------------------------------
And the implementation:
----------------------------------------
package body Demo is
procedure Inc(int_val : in out Integer) is
begin
int_val := int_val + 1;
--# assert int_val >= Integer'First and int_val = int_val~ + 1;
end Inc;
end Demo;
------------------------------
Summary:
----------------------------------------
VCs for procedure_inc :
-----------------------------------------------------------------------------
| # | From | To | Proved By | Dead Path | Status |
|-----------------------------------------------------------------------------
| 1 | start | rtc check @ 7 | Inference | No DPC | I- |
| 2 | start | assert @ 8 | Inference | No DPC | I- |
| 3 | 8 | assert @ finish | Inference | No DPC | I- |
-----------------------------------------------------------------------------
----------------------------------------
And the inferences:
----------------------------------------
@@@@@@@@@@ VC: procedure_inc_1. @@@@@@@@@@
--- Hypothesis H3 has been replaced by "true". (It is already present, as H1).
*** Proved C1: int_val + 1 >= integer__first
using hypothesis H1.
*** Proved C2: int_val + 1 <= integer__last
via its standard form, which is:
Std.Fm C2: - int_val + integer__last > 0
using hypothesis H2.
*** PROVED VC.
@@@@@@@@@@ VC: procedure_inc_2. @@@@@@@@@@
--- Hypothesis H3 has been replaced by "true". (It is already present, as H1).
%%% Simplified C2 on reading formula in, to give:
%%% C2: true
*** Proved C1: int_val + 1 >= integer__first
using hypothesis H5.
*** Proved C2: true
*** Proved C3: int_val + 1 >= integer__first
using hypothesis H5.
*** Proved C4: int_val + 1 <= integer__last
using hypothesis H6.
*** Proved C5: int_val >= integer__first
using hypothesis H1.
*** Proved C6: int_val < integer__last
using hypothesis H2.
*** PROVED VC.
@@@@@@@@@@ VC: procedure_inc_3. @@@@@@@@@@
%%% Simplified H2 on reading formula in, to give:
%%% H2: int_val = int_val~ + 1
--- Hypothesis H3 has been replaced by "true". (It is already present, as H1).
%%% Simplified H5 on reading formula in, to give:
%%% H5: int_val~ >= integer__first
%%% Simplified H6 on reading formula in, to give:
%%% H6: int_val~ < integer__last
%%% Simplified C1 on reading formula in, to give:
%%% C1: int_val = int_val~ + 1
*** Proved C1: int_val = int_val~ + 1
using hypothesis H2.
*** PROVED VC.
----------------------------------------
Phew... OK, I brought back the Divide function but changed it so that it always divides by 2. These are the VCs:
----------------------------------------
For path(s) from start to run-time check associated with statement of line 14:
function_divide_1.
H1: true .
H2: numerator >= integer__first .
H3: numerator <= integer__last .
->
C1: numerator div 2 >= integer__base__first .
C2: numerator div 2 <= integer__base__last .
C3: 2 <> 0 .
For path(s) from start to finish:
function_divide_2.
H1: true .
H2: numerator >= integer__first .
H3: numerator <= integer__last .
H4: numerator div 2 >= integer__base__first .
H5: numerator div 2 <= integer__base__last .
H6: 2 <> 0 .
->
C1: numerator div 2 = numerator div 2 .
C2: numerator div 2 >= integer__first .
C3: numerator div 2 <= integer__last .
----------------------------------------
OK, conclusion 1: Fill in missing pieces in rls-files! I added - from the Tokeneer source code:
addelementto_rules(3): integer__first may_be_replaced_by -2147483648.
addelementto_rules(4): integer__last may_be_replaced_by 2147483647.
Of course I changed them to:
multiplybytw_rules(6): integer__first may_be_replaced_by -2147483648.
multiplybytw_rules(7): integer__last may_be_replaced_by 2147483647.
Then the Examiner could prove the multiplication by two!
I neglected to mention that I changed the function to a procedure and introduced a procedure IncAndDouble that combines both procedures:
----------------------------------------
package Demo is
procedure Inc(int_val : in out Integer);
--# derives int_val from int_val;
--# pre int_val >= 0 and int_val < Integer'Last/2;
--# post int_val = int_val~ + 1;
procedure MultiplyByTwo(factor : in out Integer);
--# derives factor from factor;
--# pre factor >= 0 and factor < Integer'Last/2;
--# post factor = 2 * factor~;
procedure IncAndDouble(val : in out Integer);
--# derives val from val;
--# pre val >= 0 and val <= 100;
--# post val = 2*(val~ + 1);
end Demo;
----------------------------------------
And the implementation:
----------------------------------------
package body Demo is
procedure Inc(int_val : in out Integer) is
begin
int_val := int_val + 1;
--# assert int_val >= Integer'First and int_val = int_val~ + 1;
end Inc;
procedure MultiplyByTwo(factor : in out Integer) is
begin
factor := factor*2;
end MultiplyByTwo;
procedure IncAndDouble(val : in out Integer) is
begin
Inc(val);
MultiplyByTwo(val);
end IncAndDouble;
end Demo;
----------------------------------------
And so it needs further rules:
incanddouble_rules(6): integer__first may_be_replaced_by -2147483648.
incanddouble_rules(7): integer__last may_be_replaced_by 2147483647.
It all works!
And then I converted MultiplyByTwo back to a function:
----------------------------------------
package Demo is
procedure Inc(int_val : in out Integer);
--# derives int_val from int_val;
--# pre int_val >= 0 and int_val < Integer'Last/2;
--# post int_val = int_val~ + 1;
function MultiplyByTwo(factor : Integer) return Integer;
--# pre factor >= 0 and factor < Integer'Last/2;
--# return 2 * factor;
procedure IncAndDouble(val : in out Integer);
--# derives val from val;
--# pre val >= 0 and val <= 100;
--# post val = 2*(val~ + 1);
end Demo;
----------------------------------------
And implementation:
----------------------------------------
package body Demo is
procedure Inc(int_val : in out Integer) is
begin
int_val := int_val + 1;
--# assert int_val >= Integer'First and int_val = int_val~ + 1;
end Inc;
function MultiplyByTwo(factor : Integer) return Integer is
begin
return factor*2;
end MultiplyByTwo;
procedure IncAndDouble(val : in out Integer) is
begin
Inc(val);
val := MultiplyByTwo(val);
end IncAndDouble;
end Demo;
----------------------------------------
We can take some proofs as well:
----------------------------------------
@@@@@@@@@@ VC: procedure_inc_1. @@@@@@@@@@
*** Proved C1: int_val + 1 >= integer__first
using hypothesis H3.
-S- Applied substitution rule inc_rules(7).
This was achieved by replacing all occurrences of integer__last by:
2147483647.
~~ New H2: int_val < 1073741823
~~~~ New H4: int_val <= 2147483647
~~~~ New C2: int_val <= 2147483646
*** Proved C2: int_val <= 2147483646
using hypothesis H2.
*** PROVED VC.
@@@@@@@@@@ VC: procedure_inc_2. @@@@@@@@@@
%%% Simplified C2 on reading formula in, to give:
%%% C2: true
*** Proved C1: int_val + 1 >= integer__first
using hypothesis H5.
*** Proved C2: true
*** Proved C3: int_val + 1 >= integer__first
using hypothesis H5.
*** Proved C4: int_val + 1 <= integer__last
using hypothesis H6.
*** Proved C5: int_val >= 0
using hypothesis H1.
*** Proved C6: int_val < integer__last div 2
using hypothesis H2.
*** PROVED VC.
@@@@@@@@@@ VC: procedure_inc_3. @@@@@@@@@@
%%% Simplified H2 on reading formula in, to give:
%%% H2: int_val = int_val~ + 1
--- Hypothesis H3 has been replaced by "true". (It is already present, as H1).
%%% Simplified H5 on reading formula in, to give:
%%% H5: int_val~ >= 0
%%% Simplified H6 on reading formula in, to give:
%%% H6: int_val~ < integer__last div 2
%%% Simplified C1 on reading formula in, to give:
%%% C1: int_val = int_val~ + 1
*** Proved C1: int_val = int_val~ + 1
using hypothesis H2.
*** PROVED VC.
----------------------------------------
@@@@@@@@@@ VC: function_multiplybytwo_1. @@@@@@@@@@
-S- Applied substitution rule multiplybytw_rules(6).
This was achieved by replacing all occurrences of integer__first by:
- 2147483648.
~~~~ New H3: factor >= - 2147483648
-S- Applied substitution rule multiplybytw_rules(7).
This was achieved by replacing all occurrences of integer__last by:
2147483647.
~~~~ New H2: factor < 1073741823
~~~~ New H4: factor <= 2147483647
--- Eliminated hypothesis H3 (redundant, given H1).
--- Eliminated hypothesis H4 (redundant, given H2).
+++ New H5: integer__size >= 0
+++ New H6: integer__base__first <= integer__base__last
+++ New H7: integer__base__first <= - 2147483648
+++ New H8: integer__base__last >= 2147483647
*** Proved C1: factor * 2 >= integer__base__first
using hypotheses H1 & H7.
*** Proved C2: factor * 2 <= integer__base__last
using hypotheses H2 & H8.
*** PROVED VC.
@@@@@@@@@@ VC: function_multiplybytwo_2. @@@@@@@@@@
*** Proved C1: factor * 2 = 2 * factor
-S- Applied substitution rule multiplybytw_rules(6).
This was achieved by replacing all occurrences of integer__first by:
- 2147483648.
~~~~ New H3: factor >= - 2147483648
~~~~ New C2: factor * 2 >= - 2147483648
-S- Applied substitution rule multiplybytw_rules(7).
This was achieved by replacing all occurrences of integer__last by:
2147483647.
~~~~ New H2: factor < 1073741823
~~~~ New H4: factor <= 2147483647
~~~~ New C3: factor * 2 <= 2147483647
*** Proved C2: factor * 2 >= - 2147483648
using hypothesis H1.
*** Proved C3: factor * 2 <= 2147483647
using hypothesis H2.
*** PROVED VC.
----------------------------------------
Adding custom rules to rls files is tedious because they are overwritten when spark -vcg is invoked. Creating a file multiplybytwo.rlu with contents like this is good:
----------------------------------------
multiplybytwo_user(1): integer__first may_be_replaced_by -2147483648.
multiplybytwo_user(2): integer__last may_be_replaced_by 2147483647.
----------------------------------------
Documents used to make this tutorial:
SPARK Examiner with Run-time Checker - Generation of VCs for SPARK Programs [ pdf file ]
High Integrity Software The SPARK Approach to Safety and Security - John Barnes [ sample with 50 pages ]
SPARK Quick Reference 1-4 [ invaluable! ]
Using SPARK for a Beginnerâ€™s Course on Reasoning about Imperative Programs - Kung-Kiu Lau [ presumably I'll use this ]
http://www.uni-weimar.de/cms/fileadmin/medien/medsicherheit/Teaching/SS10/uebung_sesvs/spark_tutorial.pdf
~~