Tool Development and Support

Supplementary Release Note — The RealRTC Option

 

 

 

 

 

 

 

 

 

 

 

S.P0468.73.59

Issue: 3.5

Status: Definitive

2nd February 2009

Commercial In Confidence

DOCTYPE:Praxis title:varchar=title reference:varchar=reference status:varchar=status issue:varchar=issue date:varchar=date projectname:varchar=DocumentSet

Issue 3.5, Definitive, 2ed February 2009

073_059 Supplementary Release Note — The RealRTC Option

 

 

 

Originator

 

 

SPARK Team

 

 

 

Approver

 

 

SPARK Team Line Manager

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 



Copyright

The contents of this manual are the subject of copyright and all rights in it are reserved.  The manual may not be copied, in whole or in part, without the written consent of Praxis High Integrity Systems Limited.

 

Limited Warranty

Praxis High Integrity Systems Limited save as required by law makes no warranty or representation, either express or implied, with respect to this software, its quality, performance, merchantability or fitness for a purpose.  As a result, the licence to use this software is sold ‘as is’ and you, the purchaser, are assuming the entire risk as to its quality and performance.

Praxis High Integrity Systems Limited accepts no liability for direct, indirect, special or consequential damages nor any other legal liability whatsoever and howsoever arising resulting from any defect in the software or its documentation, even if advised of the possibility of such damages.  In particular Praxis High Integrity Systems Limited accepts no liability for any programs or data stored or processed using Praxis High Integrity Systems Limited products, including the costs of recovering such programs or data.

SPADE is a registered trademark of Praxis High Integrity Systems Limited.

Note:  The SPARK programming language is not sponsored by or affiliated with SPARC International Inc. and is not based on SPARC™ architecture.

1       Introduction

2       Generation of Run-Time Checks from Real Expressions

3       Limitations

4       Conclusion

Document Control and References

File under

Changes history

Changes forecast

Document references

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 Contents

 

 


1                       Introduction

The SPARK Examiner with Run-Time Checker is capable of generating verification conditions designed to confirm that a SPARK program is free from run-time exceptions.  In its standard form the Examiner does not generate such checks for real number expressions.  

The Examiner is capable of generating run-time checks for real expressions although the process has some limitations; this document describes the generation of such checks and their significance.

2                       Generation of Run-Time Checks from Real Expressions

The facility to generate run-time checks from real expressions is enabled by the SPARK Examiner feature “RealRTCs” in the FLEXlm licence file.  If this feature is present, an additional command line switch “realrtcs” becomes available; this can be used in addition to the “rtc” or “exp” switches described in the user manual.

3                       Limitations

When real run-time checks are produced they are generated on the basis of “perfect” arithmetic rather than the underlying arithmetic of Ada with its associated rounding errors and other imprecisions.  Furthermore, the VCs are processed by the SPADE Simplifier and Checker on this same basis.

The significance of this is that the Examiner cannot guarantee to detect real arithmetic expressions that may give rise to run-time errors  due to rounding behaviour or representational effects.  For example (and ignoring binary representation effects for clarity):

type MyReal is digits 2 range 0.0 .. 2.0;

X, Y : My Real;

...

X := 1.7;

Y := 0.145;

X := X + Y;

X := X + Y;

If the compiler rounds Y up to 0.15, say (2 digits), then adds this to X and again rounds up (2 digits of accuracy), we get X := 1.85 ® 1.9, then X := 2.05® 2.1, which is out of range, even though 1.7 + 0.145 + 0.145 is 1.99 using perfect arithmetic, which is in range. (In Ada83 the problem is even worse than shown by this example because rounding of exact halves is indeterminate!).

4                       Conclusion

Users must be aware that while the presence of an unprovable VC resulting from a real arithmetic run-time check almost certainly indicates a potential problem, the absence of unprovable VCs cannot be taken to guarantee that a run-time error will never occur

Although use of real run-time checks is of value in that it may identify errors, like testing it cannot prove their absence.  Praxis High Integrity Systems strongly recommends that a numerical analysis of a system is carried out if real run-time errors are considered an issue.

 

Document Control and References

Praxis High Integrity Systems Limited, 20 Manvers Street, Bath BA1 1PX, UK.

Copyright Praxis High Integrity Systems Limited 2009.  All rights reserved.

File under

$CVSROOT/userdocs/Examiner_SRN_RealRTC.doc (was S.P0468.73.59)

Changes history

Issue 0.1                   (15/3/99):  First draft

Issue 1.0   (16/3/99):  After formal review

Issue 1.1                   (25/7/01):  Alter originator and approver for release 5.03, and change to US Letter paper size.

Issue 2.0                   (20/3/03):  Updated to new template format

Issue 3.0                   (5/6/03):  Changes to new template, final format

Issue 3.1                   (23/11/04): Company name changed.

Issue 3.2                   (5/1/05): Actions following formal review S.P0468.79.88.

Issue 3.3                   (22/11/05): Line Manager change.

Issue 3.4 (29/11/05): Updated following review S.P0468.79.90.

Issue 3.5 (2nd February 2009): Modify copyright notice.

Changes forecast

Nil.

Document references

None.