Gem #74: Tokeneer Discovery - Lesson 4
by Dean KuoAngela Wallenburg —AltranAltran
Let's get started…
In this Gem, we will see how the SPARK tools detect any differences between a program's intended behaviour, as specified in its contract, and its actual behaviour, as implemented in the code. Thus the SPARK tools can be used either to find defects in the contract, to find defects in the implementation, to find defects in both, or to show conformance between intended and actual behaviour.
Step-by-Step Instructions
Step 1: Analyse the Correct Version of the Code
The precondition for procedure AddElementToCurrentFile in auditlog.adb (lines 772 - 774 in the code below) specifies that the array element LogFileEntries (CurrentLogFile) is less than MaxLogFileEntries and the postcondition specifies that the array element is incremented by 1.
751 procedure AddElementToCurrentFile
752 (ElementID : in AuditTypes.ElementT;
753 Severity : in AuditTypes.SeverityT;
754 User : in AuditTypes.UserTextT;
755 Description : in AuditTypes.DescriptionT)
756 --# global in Clock.Now;
757 --# in CurrentLogFile;
758 --# in out AuditSystemFault;
759 --# in out LogFiles;
760 --# in out LogFileEntries;
761 --# derives AuditSystemFault,
762 --# LogFiles from *,
763 --# Description,
764 --# LogFiles,
765 --# Clock.Now,
766 --# ElementID,
767 --# Severity,
768 --# User,
769 --# CurrentLogFile &
770 --# LogFileEntries from *,
771 --# CurrentLogFile;
772 --# pre LogFileEntries(CurrentLogFile) < MaxLogFileEntries;
773 --# post LogFileEntries(CurrentLogFile) =
774 --# LogFileEntries~(CurrentLogFile) + 1;
775
776 is
777 TheFile : File.T ;
778 begin
779 TheFile := LogFiles (CurrentLogFile);
780 AddElementToFile
781 (TheFile => TheFile,
782 ElementID => ElementID,
783 Severity => Severity,
784 User => User,
785 Description => Description);
786 LogFiles (CurrentLogFile) := TheFile;
787
788 LogFileEntries(CurrentLogFile) := LogFileEntries(CurrentLogFile) + 1;
789 end AddElementToCurrentFile;
Analyse Tokeneer with the SPARK Toolset. The result of the analysis shows (see below) that the SPARK Toolset has identified no problems with the code in the procedure AddElementToLogFile - the columns False and TO DO are empty.
659 VCs for procedure_addelementtocurrentfile : 660 ---------------------------------------------------------------------------- 661 | | | -----Proved In----- | | | 662 # | From | To | vcg | siv | plg | prv | False | TO DO | 663 ---------------------------------------------------------------------------- 664 1 | start | rtc check @ 781 | | YES | | | | | 665 2 | start | rtc check @ 782 | | YES | | | | | 666 3 | start | rtc check @ 788 | | YES | | | | | 667 4 | start | rtc check @ 790 | | YES | | | | | 668 5 | start | assert @ finish | | YES | | | | | 669 ----------------------------------------------------------------------------
Step 2: Change the Contract - But not the Implementation
Let us change the postcondition so the procedure's contract no longer matches its implementation. The SPARK Toolset will then detect the inconsistency. Change the postcondition to specify that the array element LogFileEntries(CurrentLogFile) should be incremented by 10. The modified code is shown below.
772 --# pre LogFileEntries(CurrentLogFile) < MaxLogFileEntries;
773 --# post LogFileEntries(CurrentLogFile) =
774 --# LogFileEntries~(CurrentLogFile) + 10;
775
Step 3: Re-Analyse and Study the Results
Re-analyse Tokeneer. The results of the analysis for the procedure AddElementToLogFile has changed - the columns False and TO DO are no longer empty (see below).
659 VCs for procedure_addelementtocurrentfile : 660 ---------------------------------------------------------------------------- 661 | | | -----Proved In----- | | | 662 # | From | To | vcg | siv | plg | prv | False | TO DO | 663 ---------------------------------------------------------------------------- 664 1 | start | rtc check @ 781 | | YES | | | | | 665 2 | start | rtc check @ 782 | | YES | | | | | 666 3 | start | rtc check @ 788 | | YES | | | | | 667 4 | start | rtc check @ 790 | | YES | | | | | 668 5 | start | assert @ finish | | | | | YES | | 669 ----------------------------------------------------------------------------
The SPARK Toolset has identified a potential problem with the code. The problem is that the procedure's contract and implementation don't match.
Step 4: Revert the Contract - But Change the Implementation
Undo the changes to the postcondition and change line 788 so that the input value is preserved.
774 --# pre LogFileEntries(CurrentLogFile) < MaxLogFileEntries;
775 --# post LogFileEntries(CurrentLogFile) =
776 --# LogFileEntries~(CurrentLogFile) + 1
...
791 LogFileEntries(CurrentLogFile) := LogFileEntries(CurrentLogFile) + 0;
792 end AddElementToCurrentFile;
Re-analyse Tokeneer. The analysis of the procedure is unchanged, as the implementation, like previously, does not match the procedure's contract.
Step 5: Strengthen the Contract
Revert the code to its original state.
In SPARK, we can strengthen the procedure's contract and say more about the properties of the procedure. Let's add extra code assigning the value 10 to the first element of the array LogFileEntries if CurrentLogFile is not LogFileIndexType'First (lines 789 - 791 below).
788 LogFileEntries(CurrentLogFile) := LogFileEntries(CurrentLogFile) + 1;
789 if CurrentLogFile /= LogFileIndexType'First then
790 LogFileEntries(LogFileIndexType'First) := 10;
791 end if;
792 end AddElementToCurrentFile;
Re-analyse Tokeneer and notice that no errors are reported, as the procedure's implementation is not inconsistent with its contract. The postcondition says nothing about the effects of the procedure on any of the array elements except the one indexed by CurrentLogEntry.
We can strengthen the postcondition (lines 775 and 776 below) to specify that only the entry indexed by CurrentLogFile is incremented and all other elements remain unchanged.
772 --# pre LogFileEntries(CurrentLogFile) < MaxLogFileEntries; 773 --# post LogFileEntries = LogFileEntries~[CurrentLogFile => LogFileEntries~(CurrentLogFile)+1];
Re-analyse Tokeneer and notice, on lines 659 to 671, that the mismatch between the implementation and contract has been detected.
657 VCs for procedure_addelementtocurrentfile : 658 ---------------------------------------------------------------------------- 659 | | | -----Proved In----- | | | 660 # | From | To | vcg | siv | plg | prv | False | TO DO | 661 ---------------------------------------------------------------------------- 662 1 | start | rtc check @ 783 | | YES | | | | | 663 2 | start | rtc check @ 784 | | YES | | | | | 664 3 | start | rtc check @ 790 | | YES | | | | | 665 4 | start | rtc check @ 792 | | YES | | | | | 666 5 | start | rtc check @ 794 | | YES | | | | | 667 6 | start | assert @ finish | | | | | | YES | 668 7 | start | assert @ finish | | YES | | | | | 669 ----------------------------------------------------------------------------
Summary
This Gem demonstrates that the more precise the specification, the more bugs the SPARK Toolset can detect. The use of the SPARK Toolset during development to verify code is, in our experience, more effective than compiling and testing, since the analysis is for all input data and not just a few specific test cases. In the next Gem we will see how SPARK deals with overflow errors.