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.


About the Author

Angela Wallenburg has worked as a programmer and researcher since 1998. Early in her career she developed operation control and optimization software. Since program verification captured her interest she has worked on building verification tools at Chalmers and Gothenburg University in Sweden, University of Koblenz-Landau in Germany and Microsoft Research in the US. She joined Altran and the SPARK team in 2009 to continue her quest to build really usable tools for software engineers.
Last Updated: 10/13/2017
Posted on: 11/16/2009