Home

SPARK Toolset Release Note 9

1. 15 7 15 8 PRAXIS SPARK Toolset Release Note 9 Issue 3 19 Release 6 0 November 2001 Introduction of external variables to simplify modelling of the interactions between a SPARK program and its external environment Addition of the null derives annotation to describe information flows which affect only the external environment Introduction of modular types Use of loop labels in exit statements Use of global modes on function subprograms Extended support for predefined types such as Long_Integer Simplified run time check generation for own variables Relaxation of need for mandatory type announcement of own variables Plain output option to simplify comparisons of Examiner output files Platform independent switch files and metafiles Support for intentionally infinite loops Detection of own variables that can never be initialized Detection of unusable private types Extra refinement checks on global variables when performing data flow analysis Detection of unnecessary others clause in case statements Extensions to the POGS tool Improved error messages to distinguish different cases of variables which are not declared or visible Improved SPADE Simplifier Release 2 0 New SPARKSimp Tool Release 6 1 June 2002 Introduction of tagged types Page 41 of 51 arran Tool Development and Support RN PRAXIS SPARK Toolset Release Note 9 Issue 3 19 e Introduction of type assertion annotations
2. 5 2 5 3 5 4 PRAXIS SPARK Toolset Release Note 9 Issue 3 19 Simplifier changes Simplifier 9 0 0 includes the following changes and improvements Enhanced log messages 1521 010 More informative details of substitutions that have been carried out by the Simplifier are now included in the generated SLG file SIV files are not affected by this change Increased proof coverage for partially updated composites 1424 030 Previously especially in the context of arrays the Simplifier offered limited proof automation where composite structures are partially updated by a procedure For example given an array A an index variable I and a procedure P passing A I into an out parameter of P would partially update the composite structure A The Simplifier now offers improved proof automation in these cases Simplifier uses inference rules from Examiner 1724 003 Previously the Simplifier ignored inference rules e g may_be_deduced_from rules generated by the Examiner in the RLS file if there was no corresponding RLU file The Simplifier now always tries to use inference rules from the RLS file to discharge VCs Extended Simplifier s reasoning of simple universal quantifiers with array updates 1724 016 Previously the Simplifier could not discharge VCs containing simple universal quantifiers generated by the Examiner from for loops that update an array e g initialisation of an array The Simplifier is now able to
3. 6 end P2 end Test Page 11 of 51 olT Ran C f Tool Development and Support RN PRAXIS SPARK Toolset Release Note 9 Issue 3 19 Note that the final value of Y is 6 meaning that this code does satisfy the concrete postcondition but does not satisfy the abstract postcondition stated in the package s specification The refinement VC generated for the postcondition with Examiner 8 1 4 is as follows procedure_p2_5 HL in_range x H2 x gt index_ first H3 x lt index__last H4 x lt gt element a x H5 for_all i___1 t i __1 gt index__first and i 1 lt index__last gt element a i___1 gt t__first and element a i___1 lt t__last H6 x gt t__first H7 x lt t_ last H8 a update a x x gt Gl updated a x C2 y gt s2__first C3 y lt s2__last na Note that C2 and C3 are unprovable as expected Unfortunately H4 is incorrectly generated the a should be a Furthermore H4 and H8 then form a contradiction since they reduce to x lt gt x This allows this VC to be incorrectly proved by contradiction by the Simplifier 3 4 Corrected Behaviour Examiner 9 0 0 generates the following postcondition refinement VC for the same code H1 in_range x H2 x gt index_ first H3 x lt index_ last H4 x lt gt element a x H5 for_all i___1 t i___1 gt index__first and i 1 lt index_ last
4. 6 1 PRAXIS Tool Development and Support RN SPARK Toolset Release Note 9 Issue 3 19 SPARKSimp changes New command switches and invocation of ZombieScope IC15 017 SPARKSimp now finds all vcg and dpc files in a directory tree that require analysis and applies the Simplifier to vcg files and ZombieScope to dpc files The switches nz can be used to ignore dpc files and ns can be used to ignore vcg files Release 9 0 0 of SPARKSimp has the following usage changes introduced in release 9 0 0 are highlighted in bold sparksimp a v V n ns nz t r 1 e p N x Sexec z Zexec sargs simplifier_options zargs zombiescope_options a all ignore time stamps so process all eligible files v report version and terminate V verbose output n dry run print commands but don t run Simplifier or ZombieScope ns ignore VCG files when searching nz ignore DPC files when searching t sort VCG files largest first r reverse simplification order 1l log output e echo Simpli for XXX vcg to XXX log and for YYY dpc to YYY zsl fier output to screen p N use N concurrent processes x Sexec speci fies an alternative Simplifier executable z Zexec specifies an alternative ZombieScope executable sargs pass following options in this section to Simplifier zargs pass following options in this section to ZombieScope Page 26 of 51 NS ae Tool Devel
5. e _ Introduction of modular subtypes e Introduction of the configuration file e _ Introduction of the help command line switch e Demo Examiner now runs on Linux e VCG generation for inherited operations of tagged types e Improved handling of null derives e Attributes Floor and Ceiling implemented e Detection of duplicate record fields e Improved overflow checks on universal integer expressions e Corrected handling of loop invariants in while loops e Strengthened behaviour of noecho option e Trapping non positive accuracy in real type declaration e Recursion in meta files and index files e Improved handling of Address clauses e Improved handling of Import and Interface pragmas e VCG Modelling of Boolean membership operators e Simplification of common Integer inequalities e Simplification of common enumerated inequalities e Simplification of VCs involving quantified expressions e Simplifier performance e Checker has new built in rule families MODULAR BITWISE and ENUMERATION e Proved by review option in POGS Page 42 of 51 olT Ran C i Tool Development and Support RN 15 9 15 10 15 11 PRAXIS SPARK Toolset Release Note 9 Issue 3 19 Release 6 3 December 2002 Release 6 3 of the toolset was constructed to accompany the textbook High Integrity Software The SPARK Approach to Safety and Security by John Barnes but was not delivered to other users Its main new features were e Sligh
6. 3 2 3 3 PRAXIS SPARK Toolset Release Note 9 Issue 3 19 TN IA02 023 Important Information for Users Description TN IAO2 023 concerns a case where the Examiner can generate an incorrect verification condition for a subprogram that employs refined pre and postconditions for a private type The incorrect rules mean that the Simplifier and POGS may report all VCs proved for that subprogram and calling subprograms even though a potential run time error does exist The exact circumstances for this problem to occur are as follows e The subprogram has a parameter which is a private type in the visible part of the enclosing package body e The subprogram has both abstract and concrete pre and post conditions e The enclosing package does not employ own variable state refinement so there is only one set of global and derives annotations for it In this case the refinement VC for the postcondition is essentially that concrete postcondition gt abstract postcondition This is expanded out by the Examiner into a VC of the form Abstract Precondition and Concrete Precondition and Concrete Postcondition gt Abstract Postcondition The problem lies with the Concrete Precondition section Here variables should be decorated with the oom suffix to indicate the initial value of that variable Examiners 7 2 through 8 1 4 omit this suffix in the conditions listed above leading to an incorrect VC Section
7. Remove order declaration option J121 025 and add nosli option J111 010 Issue 3 10 3rd February 2010 Default installation directory IBO3 040 Rebrand to Altran Praxis Limited Issue 3 11 8th February 2010 Update title of SPARK IO document J204 021 Issue 3 12 141th February 2010 Minor correction to 1915 022 Issue 3 13 12th February 2010 Added section 2 2 on information flow policy checking IC15 003 Issue 3 14 18th February 2010 Update Release Note J218 022 to document backward incompatibility introduced by I629 007 extended section 5 7 and added section 10 5 Issue 3 15 19th February 2010 Minor corrections to sections 5 7 and 10 5 following review Issue 3 16 22nd February 2010 Added section for SPARKSimp Issue 3 17 25th February 2010 Added section for ZombieScope and updates for release 9 0 0 Issue 3 18 1st March 2010 Replace SEPR references with TN references where possible Issue 3 19 1st March 2010 Definitive issue for release 9 0 0 following review Page 50 of 51 arran Tool Development and Support RN PRAXIS SPARK Toolset Release Note 9 Issue 3 19 Changes forecast None Document references None File under SVN trunk userdocs Release_Note_9 doc Page 51 of 51
8. Unevaluable attributes The Machine_ and Model_ attributes are accepted by the Examiner but it does not know how to statically evaluate them since they are inherently implementation dependent For example the package package F is type T is digits 6 range 10 0 10 0 C constant T Machine_Emax end F is legal SPARK but the Examiner does not know the actual numeric value of C Known error summary This section lists known errors in the Examiner that are awaiting investigation and correction 1 The SPARK rule that array actual parameters must have the same bounds as the formal parameter is not checked for function parameters where the actual parameter is a subtype of an unconstrained array type Since subtype bounds are static in SPARK errors of this kind should be detected by an Ada compiler If not an unconditional run time error will occur GEPR 1060 2 The Examiner permits the body of a subprogram to be entirely made up of proof statements thus breaching the Ada rule that at least one Ada statement must be present SEPR 278 3 Where a package declares two or more private types the Examiner permits mutual recursion between their definitions in the private part of the package SEPR 848 4 The Examiner does not take due account of a range constraint when determining the subtype of a loop variable this affects completeness checking of case statements within the loop For example for I in Integer range 1 4 loop would require
9. gt element a i__ 1 gt t__ first and element a i__1 lt t__last H6 x gt t first H7 x lt t__last H8 for_all i__1 t i___1 gt index first and i 1 lt index __last gt element a i___1 gt t__ first and element a i ___1 lt t__last H9 y gt s_ first Page 12 of 51 olT Ran C f Tool Development and Support RN 3 5 PRAXIS SPARK Toolset Release Note 9 Issue 3 19 ALO y lt s__last H11 a update a x x gt Gil updated a x C2 y gt s2_ first C3 y lt s2_ last Note that H4 is now correct and the correct range of Y is reflected in H9 and H10 The Simplifier reduces this to an unprovable VC the significant fraction of which is H7 y gt 0 H8 y lt 10 gt Cl updated update a x x x C23 y lt 5 clearly showing how the final value of Y does not imply the abstract postcondition Recommended Action For projects using Examiner 7 2 through 8 1 4 we recommend a complete back to back regression proof to check for any differences arising from this TN We also recommend that projects should check for any use of refined pre and post conditions in packages that declare private types If this language feature is not used then this problem cannot occur Please contact Praxis for further advice regarding this problem Page 13 of 51 NS ae Tool Development and Support RN attran 4 1 4 2 4 3 PRAXIS
10. 1 2nd October 2009 Added CFR 2233 SEPR 2772 TN I930 014 Page 49 of 51 arran Tool Development and Support RN PRAXIS SPARK Toolset Release Note 9 Issue 3 19 Issue 2 2 6th October 2009 Added CFR 2238 SEPR 2777 TN IA05 014 Issue 2 3 7th October 2009 Added CFR 2173 SEPR 2537 TN 1611 014 Issue 2 4 13th October 2009 Added CFR 2239 SEPR 2778 TN IAO6 016 Issue 2 5 19th October 2009 Added CFR 2246 SEPR 2785 TN IA19 002 Issue 2 6 30th October 2009 Added CFR 2241 SEPR 2780 TN IAO2 023 Issue 2 7 2nd November 2009 Added CFR 2247 SEPR 2786 TN IA19 015 Issue 2 8 3rd November 2009 Added CFR 2250 SEPR 2789 TN IBO3 014 Issue 2 9 17th November 2009 Added section 3 regarding SEPR 2780 Issue 3 0 20th November 2009 Remove Path Functions option TN IB17 027 Issue 3 1 1st December 2009 Remove Examiner rtc exp and realrtcs switches TN ICO1 020 Issue 3 2 18th December 2009 Added TN IBO4 013 Issue 3 3 22nd December 2009 Changed SEPR 712 to TN IC21 017 Issue 3 4 12th January 2010 Added section describing new SPARK Proof Manual 1929 007 Issue 3 5 17th January 2010 Added the SPARKMake language switch I A06 037 Issue 3 6 18th January 2010 Casing of the SPARK Examiner output 1422 010 Issue 3 7 21st January 2010 Added return annotations in function calls 1915 022 Issue 3 8 28th January 2010 Add Global Index J113 005 Issue 3 9 28th January 2010
11. called by function F2 Page 20 of 51 alTRan PRAXIS oOo Ta 11 12 b Tool Development and Support RN SPARK Toolset Release Note 9 Issue 3 19 function F1 X Integer return Integer pre X X lt Integer Last and X X gt 0 return X X function F2 Y Integer return Integer pre Y Y lt Integer Last and Y Y gt 0 return Y Y begin return F1 Y end F2 For path s from start to precondition check associated with statement of line 11 function f2 1 Hl H2 H3 H4 CLs C2 C3 C4 y y lt integer_ last y y gt 0 y gt integer__first y lt integer__last gt y y lt integer_ last y ay N y gt integer_ first y lt integer_ last For path s from start to finish function_f2_2 H1 I Oo OA ADA OF WwW DN y lt integer_ last x y gt 0 a gt integer_ first lt integer_ last y lt integer_ last y gt 0 gt integer_ first lt integer_ last hK KKKKKK 1 y gt integer_ first Page 21 of 51 arran Tool Development and Support RN 4 15 4 16 PRAXIS SPARK Toolset Release Note 9 Issue 3 19 ALO fFl y lt integer_ last H11 f1 y y y gt Cl fFl y y y C2 Fl y gt integer__first C3 fFl y lt integer__last In VC f2_1 the conclusions C1 and C2 are derived from the check of the pre conditions of F1 and C3 from the check that the a
12. case for unary operators Removal of Path Functions IB17 027 The ability to generate Path Functions from SPARK code is now considered obsolete and has been removed from the Examiner The Generation of Path Function manual is no longer distributed and all mention of path functions has been removed from other user manuals Page 19 of 51 arran Tool Development and Support RN 4 12 4 13 4 14 PRAXIS SPARK Toolset Release Note 9 Issue 3 19 Removal of obsolete VC Generation switches IC01 020 The rtc exp and realrtcs switches have been removed from the Examiner in favour of the new veg switch which is equivalent to the old combination exp realrtcs Existing scripts and project files must now be updated to use vcg Casing option 1422 010 A style check switch casing has been introduced which enables case sensitive checking of identifiers in SPARK code and annotations When the switch is active the Examiner will issue a warning if the use of an identifier does not match the case used in its declaration The switch takes options to enable casing checks only for identifiers declared in package Standard identifiers declared only in the program under analysis or both A related change is that the correct case is now always used when identifiers are reported in Examiner output files Users who perform a regression analysis and compare their results against those generated by an earlier version of the SPA
13. discharge VCs containing such conclusions For example consider an array A whose index and element type are both Character If we initialise A with a for loop to set each element to a value that is equal to its index position for I in Character loop A I I assert for all J in Character range Character First I gt ma A J J end loop check for all J in Character gt A J J All VCs arising from this code are now proven automatically Page 23 of 51 olT Ran C i Tool Development and Support RN 5 5 5 6 5 7 5 8 5 9 PRAXIS SPARK Toolset Release Note 9 Issue 3 19 Better reasoning for bounds of modular expressions 1805 018 The Simplifier is now able to infer the lower and upper bound for modular expressions where the modulus is up to and including 2 64 In particular this improves reasoning about programs that involve operations on 64 bit modular types Extended Simplifier s reasoning of simple universal quantifiers 1903 018 The Simplifier is now able to reason about universal quantifiers where the range is the empty set lower bound of the range is greater than the upper bound or the range is a singleton element lower and upper bounds are equal This improves the reasoning of programs with loops updating an array Enhanced management of Hypothesis Identifiers 1629 007 Refactored code that manages hypothesis identifiers SLG and SIV are affect
14. flow analysis of record fields e command line meta files e named numbers e unqualified string literals e moded global annotations and Page 39 of 51 olT Ran C i Tool Development and Support RN 15 5 15 6 PRAXIS SPARK Toolset Release Note 9 Issue 3 19 e optional information flow analysis Release 4 0 December 1998 With Release 4 0 we upgraded all users to a single product standard supporting SPARK 83 SPARK 95 and analysis options up to an including proof facilities New features were e full implementation of public and private child packages e default switch file and e provision of the INFORMED design document Release 5 0 June 2000 e Enhanced proof support facilities for proof of programs containing abstract state ll addition of quantified expressions Ill proof rule generation for enumeration types IV identification of the kind and source of each VC V suppression of trivially true VCs VI Proof Obligation Summariser tool POGS e Optional HTML output files with hyperlinks that can be browsed interactively e Better support for common Ada file naming conventions e __User selectable annotation character e Improved suppression of analysis were results might otherwise be misleading e Static expression evaluation in proof contexts e Singleton enumeration types e Revised SPARK_IO package e Error numbering Page 40 of 51 olT Ran C i Tool Development and Support RN
15. identical to SPARK95 mode Future enhancements to bring SPARK2005 only language features will follow in due course Stronger default for loop invariant 1715 017 The VC Generator has been strengthened to generate an appropriate constraint on the initial value of a for loop parameter where the iteration scheme has an explicit range constraint For example consider the following package package Loops is subtype R is Integer range 0 5 type RArray R of Integer procedure P2 A in out RArray LowB in R HighB in R derives A from A LowB HighB end Loops Page 16 of 51 olT Ran C f Tool Development and Support RN PRAXIS SPARK Toolset Release Note 9 Issue 3 19 package body Loops is procedure P2 A in out RArray LowB in R HighB in R is begin for I in Integer range LowB HighB loop A I 4 end loop end P2 end Loops Examiner 8 1 1 generated the following default loop invariant assert for all J in R gt A J in Integer and LowB in R and HighB in R and 2s I in Integer and oe I lt HighB This loop invariant is not sufficiently strong to prove the run time check VC arising from the assignment statement inside the loop body Examiner versions 8 1 4 and above correct this problem adding a single conjunct to the loop invariant that constrains relative to its initial value LowB This generates assert for al
16. only values 1 2 3 and 4 to be covered by the case statement SEPR 693 5 When summarising the counts of pragmas found during an analysis the totals may depend on whether units are selected via the command line or metafile or using the index mechanism The difference affects only pragmas placed between program units and arises because placing a file name on the command line causes the entire file to be analysed whereas selecting it using indexes causes only the required unit to be read from the file SEPR 483 Page 38 of 51 olT Ran C i Tool Development and Support RN PRAXIS SPARK Toolset Release Note 9 Issue 3 19 15 Change Summary from Release 2 0 A release note detailing changes from the previous version accompanies each toolset release this section simply summarises the various changes that have been made 15 1 Release 2 0 November 1995 Release 2 0 added e static expression evaluation e variable initialization at declaration e full range scalar subtypes and e operator renaming in package specifications 15 2 Release 2 1 July 1996 Release 2 1 added e facilities for proof of absence of run time errors 15 3 Release 2 5 March 1997 Release 2 5 was distributed with High Integrity Ada the SPARK Approach and provided initial facilities for SPARK 95 15 4 Release 3 0 September 1997 Windows NT was supported for the first time with this release Release 3 0 also added e additional SPARK 95 support e
17. 0 021 ee ecceeeeesteeeeeeneees 14 4 4 Allow use of others to initialize unconstrained array 1409 012 15 4 5 Control of path names in brief output mode I604 011 15 4 6 Index file Cache 1220 023 0 0 ceccceeeesseeeeeeeneeeceeeeeeessseeeesneeeeeseeaeees 15 4 7 New switch to select language profile I717 O14 eee 16 4 8 Stronger default for loop invariant I1715 O17 ccceesceeeeseeeeeee 16 4 9 Proof rules for record type equality I B03 018 ce eeeeeeeeeeeeeee 18 4 10 Improved error messages for undeclared operators 1930 014 19 4 11 Removal of Path Functions IB17 027 eeeeccseeeeeseeeeeeseeeeeseeeees 19 4 12 Removal of obsolete VC Generation switches ICO1 020 20 4 13 Casing option 1422 010 csccccsssssesssessseessceessssecnssesdscesssscecnssssoess 20 4 14 Return annotations in function calls 1915 022 ceeceeesteeeeee 20 4 15 SLI file generation J111 O10 ee ceeeesteesseeeseeesseeeeseessneeeseeeeeee 22 4 16 Default install directory for Windows InstallShield IBO3 040 22 5 Simplifier changes s sssssnnssnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnn nnna 23 5 1 Enhanced log messages I1521 010 ssesseesseereernnernerrnesrrnsrnrennnnns 23 5 2 Increased proof coverage for partially updated composites 1424 DOI PETAR A ET E EA E 23 5 3 Simplifier uses inference rules from Examiner 1724 003 23 5 4 Extende
18. 3 3 below shows how this error could lead to a potentially incorrect analysis SPARK Examiner versions affected This problem affects Examiner versions 7 2 December 2004 through 8 1 4 October 2009 In versions of the Examiner earlier than 7 2 refined pre and post conditions for packages with private types were not permitted Test Case The following code illustrates this problem Page 10 of 51 attran Tool Development and Support RN PRAXIS SPARK Toolset Release Note 9 Issue 3 19 package Test is type T is private type T2 is private CT constant T CT2 constant T2 subtype S is Integer range 0 10 subtype S2 is S range 0 5 function In_Range X T return Boolean function Updated A T2 X T return Boolean procedure P2 A in out T2 X in T Y out 5 derives A from A X amp Y from pre In_Range X post Updated A X and Y in S2 private type T is range 0 101 subtype Index is T range 1 10 type T2 is array Index of T CT constant T 1 CT2 constant T2 T2 others gt 1 end Test Note the abstract postcondition on P2 includes Y in S2 meaning that the exported value of Y must lie in the range O through 5 The body of the package is as follows package body Test is procedure P2 A in out T2 X in T Y out S pre X in Index and X A X post A A X gt X is begin A X X Y
19. 3 5 Checker Rules Manu alisssciseiass cosecave cassenss cass cevsscevsans aaa 34 13 6 SPARKMake User Manual c cceeseccecsseeeeeeseeeeeeseaecessseeesesneeeenseaeees 34 13 7 SPARKFormat User Manuals sisisi nran 34 13 8 SIMPITC his vite iinien edict cla wien edinniiieh water rE NNE 34 13 9 ZombieScope User Manual ccecseccecssccecesseeceeeeeeeeseseeeseeseeeesseaeees 34 1331 0 POGS User MARU cc scs tect cxseiete aa a Coady dane ccltlans aA 34 13 22 SPARK Proof MamuUalll asics ca ics cette inacsicssceceiasinacedsoceacodvecnacedancdedvaca tensesea is 34 13 12 SPARK Quick Reference Guide 5 uu ceceeeeeeeeeeeeeneeeeeeeeeeeeesteeeesenaees 34 13 13 SPARK Quick Reference Guide 6 eececeeeeeeeeeeneeeseeeeeeeesteeeesenaees 34 13 14 INFORMED Design Method for SPARK sccsscsstecsseessessereeeeeeees 35 13 15 SPARK IO Input Output for SPARK Programs cccceeseeeeeeeeees 35 14 Limitations and known errors 0ssssssssssssesseeseseeees 36 14 1 TOOL WMMMATIONS sisira tisadi na Eaa anaia sa EnEV aY 36 14 2 Known error SUMIMALY ssssssssssssssssnnnsennnnnrnnnrnnnnnnnnnnnnnnnnnnnnnnnannnnnnn ennnen 38 15 Change Summary from Release 2 0 s sssssssnnnnnnnnnnnnnnnnnnnnnnn 39 Page 4 of 51 olT Ran C f Tool Development and Support RN PRAXIS SPARK Toolset Release Note 9 Issue 3 19 15 1 Release 2 0 November 1995 ccccccssssssececeeessssseeseseeessssseneeeees 39 15 2 Release 2 1 July 1996 srira a
20. Issue 0 6 3rd July 2009 Update for new brief switch behaviour SEPR 2718 Issue 0 7 3rd July 2009 Update for new index file search behaviour SEPR 2594 Issue 0 8 8th July 2009 Updates following review S P0468 7 190 Issue 0 9 17th July 2009 Updates following review S P0468 7 61 Issue 1 0 20th July 2009 Update for new language switch SEPR 2738 Issue 1 1 28th July 2009 Updates for release 8 1 3 Issue 1 2 28th July 2009 Updates following review 7 200 Issue 1 3 29th July 2009 Add section 4 3 describing SEPR 2744 Issue 1 4 4th August 2009 Add section 3 8 describing SEPR 2747 Issue 1 5 6th August 2009 Add section 3 9 describing SEPR 2748 Issue 1 6 24th August 2009 Added section 5 1 describing TN820 002 and sections 5 2 and 9 2 describing TN820 003 Issue 1 7 28th August 2009 Added section 4 5 describing TN805 018 Issue 1 8 11th September 2009 Added sections 5 1 5 2 and 9 describing TN820 003 Issue 1 9 14th September 2009 Finalised release number as 8 1 4 for release candidate 1 Issue 1 10 15th September 2009 Added section 4 6 describing TN 903 018 Issue 1 11 18th September 2009 Added warning control file key index_manager_duplicates User manual changes section Issue 1 12 25th September 2009 Definitive issue for 8 1 4 following review S P0468 7 221 Issue 2 0 1st October 2009 Added CFR 2203 SEPR 2743 TN I727 020 and SFR 2187 SEPR 2728 TN 1629 007 Issue 2
21. RK Toolset are likely to see a large number of differences due to the correct casing now being used in output files For more information on the use of this switch see the Examiner User Manual Return annotations in function calls 1915 022 Function return annotations are now translated and incorporated in the hypotheses of paths that traverse the function call It is no longer necessary to provide a user defined rule to specify the function within the proof tools User defined rules may still be required to specify properties resulting from the definition given in the return annotation For VC generation a function call is modelled by 1 a check statement to show that all actual parameters are in in type global variables of a function are assumed to be in type as they are checked prior to the function call existing behaviour 2 a check statement to show that the pre condition of the called function is satisfied by the actual parameters used and the current values of the called function s global variables existing behaviour 3 anassumption which appears in the hypotheses of VCs for paths which traverse the function call that the function s return annotation holds for the given actual parameters including global variables new behaviour and 4 an assumption that the returned value is in type existing behaviour For example the following function declaration F1 with an explicit return annotation gives the VCs shown when it is
22. RK2005 Reserved Words SEPR 2778 The language profile for SPARK2005 Examiner switch language 2005 now supports the use of the Ada2005 reserved words interface overriding and synchronized In SPARK2005 mode these are treated as reserved words In SPARK95 mode these are treated as identifiers but a warning is issued as before In SPARK83 mode these are treated as identifiers and no warning is issued Functional Attribute S Mod SEPR 2786 The language profile for SPARK2005 implements the functional attribute S Mod that was introduced in Ada2005 See the Ada2005 LRM section 3 5 4 16 for more details The expression S Mod X iS expanded by the VC Generator into the equivalent FDL X mod S Modulus Functional Attribute S Machine_Rounding SEPR 2789 In SPARK 2005 mode the Examiner now accepts the attribute Machine_Rounding for floating point types However similar to the attribute Rounding the Examiner will raise semantic error 30 attribute Machine_Rounding is not yet implemented in the Examiner Optional Overriding_Indicator IBO4 013 In SPARK 2005 mode a subprogram specification of a type extension of a tagged type is subject to the following rules e The subprogram must be prefixed with the reserved word overriding if it is an inherited operation e The subprogram specification is optionally prefixed with the reserved words not overriding if it is not an inherited operation that is not overriding is
23. SPARK Toolset Release Note 9 Issue 3 19 Examiner changes This section documents other significant changes to the SPARK Examiner made for release 9 0 0 Where appropriate GNAT Tracker Ticket Numbers TNs are given Allow labels on statements 1521 014 As described in section 2 1 the SPARK language now permits labels so the SPARK Examiner has been updated accordingly to recognise and accept labelled statements It should be noted that the Examiner checks the syntax of labels but otherwise ignores them as they have no effect on the semantics of the SPARK program As such it does not perform any semantic checks for example it will not check whether a label s identifier clashes with other identifiers in scope These checks will be performed by an Ada compiler Allow proof refinement where applicable 1309 006 Previously it was not possible to perform proof refinement of functions where the sole justification for the refinement was the function returning a private type Further where using subunits it was never possible to perform proof refinement of functions These two cases are resolved such that proof refinement is now possible if it is applicable Output Directory in report file 1610 021 The Examiner s report file now includes both the requested and actual output directory When the plain switch is active the requested directory is repeated in both cases to avoid spurious differences in regression analysis For example t
24. a 39 15 3 Release 2 5 March 1997 cccsscccccecessssssceseceseesensensecesasscanseeeenees 39 15 4 Release 3 0 September 1997 cescsseeecssecsseessesserseeseesseresseeens 39 15 5 Release 4 0 December 1998 0 eee ceccceeeesseceeeeeeeeenseeeeeesneeeesenaeees 40 15 6 Release 5 0 June 2000 ssirissrirr sirrinin iseanan aianei 40 15 7 Release 6 0 November 2001 1 ccccccssssssceceeesssssaeseeeeesssssanseeees 41 15 8 Release 6 1 June 2002 snnnssnnnnnnnsrennnnnnrrrnnnnnnnrrnnnnnnnnrnnnnnnnnnren nenna 41 15 9 Release 6 3 December 2002 ceccccceeessceeeeneeeesseeeeeeseneeeneeeeees 43 15 10 Release 7 0 July 2003er oaea aa a ERa Ear 43 15 11 Release 7 2 December 2004 cccccssssececesessssseeeceseesessssneeeeeeees 43 15 12 Release 7 3 February 2006 0 eeeeececesceeeeeeeeeeeeeeaeeeenseeeeeesieeeeseeaees 44 15 13 Release 7 31 April 2006 c cc eccccccssceceessecesssseececsseeeseesseeessneeees 45 15 14 Release 7 4 January 2007 ccesccsstecseesseessseeesseecseeeesneesseneeeeesse 45 15 15 Release 7 5 May 200 f os csscisccescicvecescsccvissceauseessvssiecscvsvecesesdsssvsveceess 46 15 16 Release 7 6 June 2008 ccsccccececesssssseeseceseessnssensecesessensnenseeees 46 15 17 Release 7 6 2 February 2009 ccccceeeeeseeeeeeeeeeessseeeeessseeeeseaeees 47 15 18 Release 8 1 0 March 2009 cccccccccecssssssececeeesssssaeseseeesssssseseeeees 47 15 19 Release 8 1 1 May 2009 ccccccccc
25. although aggregates of arrays of arrays can SEPR 590 Page 36 of 51 arrant PRAXIS 14 1 3 Attribute limitations Tool Development and Support RN SPARK Toolset Release Note 9 Issue 3 19 Verification conditions involving real numbers are evaluated using infinite precision or perfect arithmetic this allows the correctness of an algorithm to be shown but cannot guard against the effects of cumulative rounding errors for example The Examiner does not generate VCs for package initialization parts Statically determinable constraint errors will be detected during well formation checking of package initialization SEPR 288 The VC Generator cannot model the implementation dependent attributes of floating and fixed point types see section 14 1 3 14 1 3 141 Unimplemented attributes The following attributes are officially supported by SPARK according to the language definition but are not yet implemented by the Examiner The Examiner will generate error number 30 Attribute XXX is not yet implemented in the Examiner if you try to use them Adjacent Compose Copy_Sign Leading_Part Remainder Scaling Exponent Fraction Machine Machine_Rounding Model Rounding Truncation Unbiased_Rounding Page 37 of 51 NS ae Tool Development and Support RN attran 14 1 3 2 14 2 PRAXIS SPARK Toolset Release Note 9 Issue 3 19 Note that these are all function like attributes concerning floating and fixed point types
26. amrant PRAXIS MS Tool Development and Support SPARK Toolset Release Note 9 RN Issue 3 19 Status Definitive 1st March 2010 Originator SPARK Team Approver SPARK Team Line Manager olT Ran C f Tool Development and Support RN PRAXIS SPARK Toolset Release Note 9 Issue 3 19 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 Altran Praxis Limited Limited Warranty Altran Praxis 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 Altran Praxis Limited accepts no liability for direct indirect special or consequential damages nor any other legal liability wnatsoever and howsoever arising resulting from any defect in the software or its documentation even if advised of the possibility of such damages In particular Altran Praxis Limited accepts no liability for any programs or data stored or processed using Altran Praxis Limited products including the costs of recovering such programs or data SPADE is a trademark of Altran Praxis Limited Note The SPARK programming language is not sponsore
27. and Support RN 16 16 1 16 2 16 3 16 4 16 5 PRAXIS SPARK Toolset Release Note 9 Issue 3 19 Operating system compatibility VAX VMS The toolset is no longer available on VAX VMS SPARC Solaris The toolset is compatible with Solaris 8 through to 10 including those with a 64 bit kernel n b Solaris 6 and 7 are no longer supported Windows The toolset is compatible with Windows XP Windows 7 Server 2003 32 bit Vista and 64 bit Vista Intel Linux The toolset is compatible with Intel x86 based Linux operating systems in both 32 bit and 64 bit versions The toolset is built tested and packaged on RedHat Enterprise Linux 4 7 Other distributions may work but are not formally supported Apple OS X The toolset is compatible with Apple s Intel based OS X Darwin operating systems The toolset is built and tested on OS X version 10 5 8 Page 48 of 51 arran Tool Development and Support RN PRAXIS SPARK Toolset Release Note 9 Issue 3 19 Document Control and References Altran Praxis Limited 20 Manvers Street Bath BA1 1PX UK Copyright Altran Praxis Limited 2010 All rights reserved Changes history Issue 0 1 29th May 2009 First draft for release 8 1 2 Issue 0 2 2nd June 2009 Updates following review S P0468 7 168 Issue 0 3 11th June 2009 Draft for changes post 8 1 2 release Issue 0 4 18th June 2009 Update for SEPR 2713 Issue 0 5 1st July 2009 Update for SEPR 2723
28. anual Remove order declaration option Simplifier Updated section for SPARKSimp to include switches for ZombieScope removed Path Functions and updates due to changes to the Simplifier ZombieScope User Manual Added user manual for ZombieScope POGS User Manual Update document for changes to POGS including the processing of ZombieScope files SPARK Proof Manual This document replaces the manuals Generation of VCs for SPARK Programs and Generation of RTCs for SPARK Programs This should reduce the potential for confusion over which document to consult on a particular topic relating to SPARK proof SPARK Quick Reference Guide 5 New quick reference guide of Proof Checker Commands SPARK Quick Reference Guide 6 New quick reference guide for the Proof Checker Rules Page 34 of 51 OlTRAaNn C i Tool Development and Support RN PRAXIS SPARK Toolset Release Note 9 Issue 3 19 13 14 INFORMED Design Method for SPARK Corrected a cross reference 13 15 SPARK IO Input Output for SPARK Programs Now states that SPARK_IO may be used with SPARK95 and SPARK2005 Page 35 of 51 NS ae Tool Development and Support RN attran PRAXIS SPARK Toolset Release Note 9 Issue 3 19 14 Limitations and known errors 14 1 Tool limitations This section describes limitations of the Examiner tool arising mainly from incomplete implementation of planned features Where appropriate a SPARK Examiner Performance Re
29. cessssssseceesessssaeeeseceesessssneeeeeeees 47 16 Operating system compatibility ssceessssssssseseeeeees 48 16 1 VAXNMS excise eere estadioan e eE aE aa a a NaRa RRi 48 16 2 SPARC SOlANS ara eiei taea esa inao aE aa akaraia E e E eapi EN EEEE 48 163 WING OWS e a a ra aea E aa EE eE A E ssoerdeesiaties 48 TOA Intel LiNUK sona ane eaea e a SieesGvnstec ates OENE AE ERSE 48 16 5 Apple OS X sirrien arer area Ear Ea aeea EREET ir E E LENEE 48 Document Control and References ssssssssnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnn 49 Changes HIStory orrs raaa o aa aaa EE caesar 49 AELE s E E E E EE 51 Document FefEreNCeS c cccccessesssecesecessessnansececesessneesececassesscansesecaseesenanee 51 File Unde sosea a 51 Page 5 of 51 NS ae Tool Development and Support RN attran PRAXIS SPARK Toolset Release Note 9 Issue 3 19 1 Introduction Continued development of the SPARK Toolset has resulted in the development of a number of useful features that have been incorporated into Toolset Release 9 0 0 This document describes changes in the behaviour of all variants of the SPARK Toolset Release 9 0 0 compared to Release 8 1 1 Page 6 of 51 NS ae Tool Development and Support RN attran 2 1 2 1 1 2 1 2 2 1 3 2 1 4 PRAXIS SPARK Toolset Release Note 9 Issue 3 19 SPARK language changes This section describes SPARK language changes supported by Toolset Release 9 0 0 since release 8 1 1 SPARK 2005 SPA
30. ctual parameter Y is in type This VC has to be proved to show that the preconditions of F1 are satisfied by this call The hypotheses in VC f2_2 H3 and H4 follow from the in type check of the actual parameter Y H5 and H6 follow from the precondition check for the call to F1 H9 and H10 are the assumptions that the returned value from F1 is in type and H11 is the assumption that the return annotation of F1 is satisfied SLI file generation J111 010 The SPARK Examiner now generates SLI files by default for cross navigation in an IDE e g GPS or Emacs or using the GNATFind tool For each SPARK source file that is analysed the Examiner now generates a corresponding SLI file with the extension sli A new switch nosli has been added in order to suppress generation of SLI files if they are not required The new warning Warning 430 SLI generation abandoned owing to syntax or semantic errors or multiple units in a single source file will be raised if there is a syntax or a semantic error in the SPARK source code or if a file contains multiple compilation units Once this warning has been produced no more SLI files will be generated Default install directory for Windows InstallShield IBO3 040 By default the tools are installed to C SPARK lt version gt when using the Windows InstallShield executable The previous default was C Spark lt version gt Page 22 of 51 NS ae Tool Development and Support RN arran 5 1
31. d realrtcs switches IC01 020 The Examiner switches rtc exp and realrtcs have been removed and replaced by the single vcg switch Existing default switch files scripts and project files will have to be updated Remove order declaration option in SPARKFormat J121 025 The SPARKFormat switch order declaration has been removed By default SPARKFormat uses alphabetical order to reformat annotations Enhanced management of Hypothesis Identifiers 1629 007 This change can change the hypothesis identifier assigned to a derived hypothesis and can affect the Simplifier s search for proofs when it relies on user rules that contain free variables in side conditions The use of free variables in side conditions is generally not recommended unless it is essential When used it is recommended that a more constrained expression containing the free variable precede less constrained expressions containing the free variable Page 32 of 51 olT Ran C i Tool Development and Support RN 13 13 1 13 2 13 3 13 4 PRAXIS SPARK Toolset Release Note 9 Issue 3 19 User manual change summary The following user manuals have been changed between Examiner Releases 8 1 1 and 9 0 0 New Global Documentation Index A new Global Index is supplied with the toolset documentation This is supplied in both PDF and HTML formats with filenames Global_Index pdf and Global_Index htm respectively This forms a one page index
32. d Simplifier s reasoning of simple universal quantifiers with array updates 1724 016 eesecseecesecseeesseesserseeseecsereesseesseneeeneeees 23 5 5 Better reasoning for bounds of modular expressions 1805 018 24 5 6 Extended Simplifier s reasoning of simple universal quantifiers WOO SEO TS EEE tect coves accused saan nacesubs cress E A E 24 5 7 Enhanced management of Hypothesis Identifiers I629 007 24 5 8 Improved readability of Simplifier verbose mode output 1727 020 E aie nivite ai va E E EE 24 5 9 Improved support for disjunctions 1611 014 oo eeeeeeeeeeeee 24 5 10 Improved reasoning of empty ranges in universal quantified VCs NAI 002 irian nnana aa ana E a a EEEE EOE 25 Page 3 of 51 olT Ran C i Tool Development and Support RN PRAXIS SPARK Toolset Release Note 9 Issue 3 19 6 SPARKSI Mp changes cccccccsssseeeeeeceeeeenseseeneneneeeeessesensnenaeeees 26 6 1 New command switches and invocation of ZombieScope IC15 017 T E E A cu sobewscnebaate E exe ates aseatavocnek testes 26 7 Proof Checker changes sssccssssccsssseccesseseeeessnseeesesnseeeeesnneees 27 7 1 New replace_more flag lIB20 O02 eeeececeeeeseeeeeeseeeeesseeeeeeneee 27 7 2 Improved reasoning of false hypothesis 1820 003 27 8 POGS CHANBCS wiccsincssciccceetece cones cceeccccnsesesscsceetccccessesdsenccanccosszes 28 8 1 Preserve casing when reporting files used I605 005 ee 28 8 2 Extended POGS to process Z
33. d by or affiliated with SPARC International Inc and is not based on SPARC architecture Page 2 of 51 olT Ran C f Tool Development and Support RN PRAXIS SPARK Toolset Release Note 9 Issue 3 19 Contents 1 lntr d tti i cesses cc ccetics ficccetce caste seneitewe cnncencdeneteeeceneedce exeecesedaweeeee 6 2 SPARK language Changes sssssscccsssseeeeeccceeeesssseeeeseneeeenss 7 21 SPARK ZOO Dak a aa aaraa anea aa eae fava sSrndieesansnuccdesscdmsssnsedentuusvaacsoeds 7 2 2 Checking safety and security policies using flow analysis IC15 003 E E disaster teen nein Wari Dive E Wnt ees 8 2 3 Allow labels on statements in SPARK SEPR 2703 nsss 8 2 4 Allow use of others to initialize unconstrained array SEPR 2723 8 3 TN IA02 023 Important Information for Users 000000 10 3 1 DESCrIPUON sc ceiisseties coastacd aiitavi esti deiabevtav aves evsensetiveceetscen eaves ave NEY 10 3 2 SPARK Examiner versions affected cccccsccccsscceceeseceeeeeneeeeenseeeeees 10 Bid TSU CASE E EE A E ETET 10 3 4 Corrected Behaviour cscccssessssseeesessssseseeesssseseneesseseeseessseseseessaees 12 3 5 Rec mmended AGOM essaiar aanraai 13 4 Examiner changeS s sssssssssennnnnnnennnnnnnnnnnnnnnnnnnnnnnn nnmnnn nnmnnn 14 4 1 Allow labels on statements 1521 014 ooo ececssecssreeesteesseeeeseeeeee 14 4 2 Allow proof refinement where applicable I309 006 eee 14 4 3 Output Directory in report file I6 1
34. ed by the change but not log files Added support for norenum flag The hypothesis and conclusion identifiers are not renumbered in siv files and provides better tracing of hypothesis and conclusions from a siv file to the veg file This change can change the hypothesis identifier assigned to a derived hypothesis and can affect the Simplifier s search for proofs when it relies on user rules that contain free variables in side conditions The use of free variables in side conditions is generally not recommended unless it is essential When used it is recommended that a more constrained expression containing the free variable precede less constrained expressions containing the free variable Improved readability of Simplifier verbose mode output 1727 020 Improved output message in verbose mode Improved support for disjunctions 1611 014 The Simplifier now provides improved support for reasoning of disjunctions in hypothesis and conclusions Previously the Simplifier was unable to discharge VCs of the form shown below H1 x or y gt Cl yorx Page 24 of 51 RN attranl Tool Development and Support Issue 3 19 PRAXIS SPARK Toolset Release Note 9 5 10 Improved reasoning of empty ranges in universal quantified VCs 1A19 002 The Simplifier now discharges all conclusions of the form for_all iI T LWB lt I and I lt UPB gt X where the range is the empty range that is UPB lt LWB Page 25 of 51 amrant
35. ffending file in any error or warning messages This is useful when a project has multiple source directories and not all source files are therefore in the current working directory brief alone is equivalent to brief nopath Index file cache 1220 023 An index file cache has been introduced to speed up the generation of cross references within annotations for future integration into IDEs The operation of the cache means that the behaviour of the Examiner when reading index files may be different The new behaviour is described in the Examiner User Manual In particular it should be noted that the behaviour has changed in the following ways 1 The order of auxindex entries within a file is now immaterial 2 If a unit cannot be found within the auxiliary index files associated with an auxindex entry with a matching prefix the search will continue and if necessary proceed with searching the super index file if one is specified The different behaviour means that the following entries in an index file are now permissible new_behaviour idx superindex is in super idx P auxindex is in p_aux idx Should not contain P A B specification P A auxindex is in p a_aux idx Should not contain P A B specification P A B specification is in p a b ads If the required unit is P A B specification then this will be found in index file new_behaviour idx If the required unit is P A C and it is defined in P A auxindex but not in P a
36. flow analysis of array element out parameters Port of Demo toolset to Mac OS X New typecheck option in Simplifier Improved validity checking of user defined proof rules in the Simplifier Correction to ARITH proof rules in the Checker Release 7 4 January 2007 Release 7 4 of the toolset comprised Examiner version 7 4 Simplifier 2 30 Checker 2 08 Page 45 of 51 arran Tool Development and Support RN 15 15 15 16 PRAXIS SPARK Toolset Release Note 9 Issue 3 19 Significant features of this release included e The accept annotation e Conditional flow errors are now reported as errors e The Simplifier supports user defined proof rules e SPARKFormat supports a wider range of annotations e SPARKMake has the ability to generate relative pathnames Release 7 5 May 2007 Release 7 5 of the toolset comprised Examiner version 7 5 Simplifier 2 32 Checker 2 08 Significant features of this release included e Correct VC generation for record fields and array elements used as in or in out parameters Release 7 6 June 2008 Release 7 6 of the toolset comprised Examiner version 7 6 Simplifier 2 39 Checker 2 11 Significant features of this release included e Allows single field record type to be Atomic in RavenSPARK mode e Simpler modelling of Character Pos and Val in VCs e Better modelling of S Valid where S is a subtype e New Output_Directory option
37. for major topics covered in all the other manuals and documents The PDF and HTML versions of the index contain hyperlinks that lead to the referenced manuals SPARK Language Definitions The SPARK Language Definitions have been renamed and unified in this release to form two documents e SPARK83_LRM this is the language reference manual for SPARK83 only e SPARK_LRM this is the language reference manual for SPARK95 and SPARK2005 including both the sequential and ravenscar concurrency profiles Examiner User Manual e Added warning control keyword index_manager_duplicates for suppressing warnings regarding index file duplicate entries e Added description of new casing switch e Added nosli switch Checker User Manual The Replace More prompt is now controlled by a new flag replace_more which is off disabled by default A new feature has been introduced to automatically infer a conclusion from a false hypothesis This feature is controlled by the flag auto_infer_from_false that is on enabling the feature by default Page 33 of 51 NS ae Tool Development and Support RN arran 13 5 13 6 13 7 13 8 13 9 13 10 13 11 13 12 13 13 PRAXIS SPARK Toolset Release Note 9 Issue 3 19 Checker Rules Manual Update copyright and licence information in listings of proof rule files SPARKMake User Manual Documents the use of the new language_profile switch SPARKFormat User M
38. for the Examiner Page 46 of 51 olT Ran C i Tool Development and Support RN 15 17 15 18 15 19 PRAXIS SPARK Toolset Release Note 9 Issue 3 19 e New Order option for SPARKFormat Release 7 6 2 February 2009 From release 7 6 2 of the toolset the version numbers of all the SPARK tools were made consistent ie all tools had the version number 7 6 2 This was an interim release the significant feature being the correction to SEPR 2517 All users were informed of the availability of this release and it was made available on demand As the majority of users did not take this release the changes detailed in the release note for 7 6 2 were also included in the release note for 8 1 0 Release 8 1 0 March 2009 Significant features of this release included e New vcg and noswitch Examiner switches e Documentation of the Examiner s debug switch e Significantly improved Simplifier performance e New platforms supported in SPARK Pro 32 bit Linux 64 bit Linux Apple OS X Release 8 1 1 May 2009 Significant features of this release included e Examiner now warns if vcg specified but no VCs generated e Additional proof rules for task discriminants e Correction to modelling of dynamic for loop nested inside case statement e FDL declarations and rules for numeric constants used in proof rules e New debug V switch for visualization of VCG graphs Page 47 of 51 olT Ran C i Tool Development
39. generate an additional proof rule in the RLS file A B may_be_deduced_from goal checktype A r E goal checktype B r fld_fl A fld_f1 B fld_f2 A fld_f2 B Page 18 of 51 olT Ran C i Tool Development and Support RN 4 10 4 11 PRAXIS SPARK Toolset Release Note 9 Issue 3 19 This rule is effectively an instantiation of the more general Proof Checker rule family RECORD_EQUALITY see Proof Checker Rules Manual section 4 13 for type R Simplifier 8 1 4 and above are able to take advantage of such rules to prove conclusions like the one shown above automatically Improved error messages for undeclared operators 1930 014 Consider the following code type T is mod 2 32 procedure Op X Y in Tr Z out T derives Z from X Y post Z X or Y The postcondition parses as Z X or Y owing to the lower precedence of or so this expression is illegal since there is no or operator that takes Boolean on the left and type T on the right Examiner 8 1 4 reported post Z X or Y A xxx Semantic Error 35 Operator is not declared for these types In Examiner 9 0 0 this error message has been improved to indicate the types found thus post Z X or Y A xxx Semantic Error 35 Binary operator is not declared for types BOOLEAN and T Secondly a new semantic error 119 has been added that covers the same
40. gt gt null end if label not permitted her end Increment Note that labels are also permitted to appear before pragmas but declarations and SPARK annotations may not be labelled For more information on labels please refer to the Ada Language Reference Manual section 5 1 and the SPARK Language Definition docs PDF SPARK95 pdf under your SPARK Toolset installation directory Allow use of others to initialize unconstrained array SEPR 2723 SPARK now permits the use of an unqualified aggregate assignment to initialize an unconstrained array parameter provided that e the aggregate only specifies a value for others e the array is one dimensional ie multi dimensional unconstrained arrays cannot be initialized in this way at present Page 8 of 51 arran Tool Development and Support RN PRAXIS SPARK Toolset Release Note 9 Issue 3 19 For example type A is array Integer range lt gt of Integer procedure Init_Array X out A derives X from is begin X others gt 0 end InitArray Note that the use of an unconstrained array type name to qualify an aggregate is not permitted in Ada but it may now be used in SPARK annotations so that a suitable postcondition can be written for the example above thus procedure Init_Array X out A derives X from post X A others gt 0 Page 9 of 51 olT Ran C i Tool Development and Support RN 3 1
41. he table below shows the output in the report file for running the Examiner with the given options assuming that current working directory is d sparkdev examiner Options Report file output output_directory requested output_directory actual D sparkdev examiner plain output_directory requested output_directory actual output output_directory requested output_directory actual D sparkdev plain output output_directory requested output_directory actual Page 14 of 51 olT Ran C i Tool Development and Support RN 4 4 4 5 4 6 PRAXIS SPARK Toolset Release Note 9 Issue 3 19 Allow use of others to initialize unconstrained array 1409 012 The Examiner has been updated in line with the SPARK language change described in section 2 4 Control of path names in brief output mode 1604 011 The brief switch has been extended to allow control over the path names generated in error and warning messages The brief switch may now take an optional value which must be nopath or fullpath nopath corresponds with the behaviour of brief in all existing Examiner versions prior to 8 1 4 and remains the default In this mode the Examiner reports the base name of the offending file without any path or directory information When fullpath is selected the Examiner includes the full path name of the o
42. l J in R gt A J in Integer and LowB in R and HighB in R and E I in Integer and e I gt LowB and I lt HighB and all VCs are automatically discharged by the Simplifier The same improvement applies to for loops with an in reverse iteration scheme where the right hand side of the range constraint is used as the initial value of the loop parameter Page 17 of 51 olT Ran C f Tool Development and Support RN PRAXIS SPARK Toolset Release Note 9 Issue 3 19 4 9 Proof rules for record type equality 1803 018 The VC Generator has been improved to generate an inference rule for equality of record types This appears in the RLS file and can be exploited by Simplifier 8 1 4 and above to prove VCs involving equality between record objects updates of those objects and aggregate expressions Consider the following record type and subprogram declaration type R is record Fl Integer F2 Boolean end record procedure Init X out R derives X from post X R F1 gt 0 F2 gt False The body of Init is implemented thus procedure Init X out R is T 2 Ry begin T F1 0 T F2 False X T end Init which results in the following VC conclusion C1 upf_f2 upf_fl t 0 false mk__r fl 0 f2 false Simplifier 8 1 3 was not capable of proving this conclusion automatically Examiner 8 1 4 and above now
43. ly across all platforms Extended POGS to process ZombieScope files and enhanced POGS output IBO5 012 POGS has been extended to process ZombieScope files dpc and sdp and report dead paths analysis The header and the per subprogram analysis sections of POGS have been updated to improve the readability and searchability of POGS Summary files For full details refer to the POGS user manual Page 28 of 51 olT Ran C i Tool Development and Support RN 9 1 PRAXIS SPARK Toolset Release Note 9 Issue 3 19 SPARKFormat changes SPARKFormat version 9 0 0 includes the following changes and improvements Remove order declaration option J121 025 The option order declaration has been removed so annotations are now always output in alphabetic order after reformatting The option order alphabetic is still supported but is no longer required as it is the default behaviour Page 29 of 51 olT Ran C i Tool Development and Support RN PRAXIS SPARK Toolset Release Note 9 Issue 3 19 10 SPARKMake changes SPARKMake 9 0 0 includes the following changes and improvements 10 1 Language selection switch IA16 037 A new switch allows selection of the sequential language profile It takes the form language 83 95 2005 The default is SPARK95 The language switch is required if your program is written in SPARK83 or SPARK2005 and uses features that would cause it to be rejected by SPARKMake when running in SPARK95
44. mode For more information see the SPARKMake User Manual Page 30 of 51 arran Tool Development and Support RN PRAXIS SPARK Toolset Release Note 9 Issue 3 19 11 ZombieScope Changes ZombieScope 9 0 0 includes the following changes and improvements 11 1 Distribution of ZombieScope Inclusion of the ZombieScope tool in SPARK Pro 9 0 0 ZombieScope detects dead paths in SPARK source code see ZombieScope user manual for further information Page 31 of 51 NS ae Tool Development and Support RN arran 12 12 1 12 2 12 3 12 4 12 5 PRAXIS SPARK Toolset Release Note 9 Issue 3 19 Backward incompatibilities The following backward incompatibilities were introduced between Examiner Releases 8 1 1 and 9 0 0 Checker Replace_more prompt I820 002 The change can break existing Checker command scripts and they will need to be updated The prompt Replace more after a replace command has been removed For backward compatibility set the replace_more flag to on This can be done via the set command as described in the Proof Checker User Manual section 5 2 6 Improved reasoning of false hypothesis I820 003 This change can break existing Checker command scripts and they will need to be updated The easiest solution is to set the auto_infer_from_false flag to off This can be done via the set command as described in the Proof Checker User Manual section 5 2 6 Removal of rtc exp an
45. of contexts Extra hypotheses for local variables Suppression of VC generation for illegal function bodies Replacement rules for composite constants Concurrent simplification with SPARKSimp Improved simplification of VCs with large structured objects Improved simplification of arithmetic and logical expressions New SPARKMake tool Release 7 3 February 2006 Release 7 3 of the toolset comprised Examiner version 7 3 Simplifier 2 22 Checker 2 06 Significant features of this release included Improved VC Generation New error explanations switch for Examiner Generation of proof rules for Size Improved diagnosis and reporting of common syntax errors Page 44 of 51 olT Ran C i Tool Development and Support RN 15 13 15 14 PRAXIS SPARK Toolset Release Note 9 Issue 3 19 Error and warning count summary in Examiner output Use of pragma Import to complete an external own variable Correction to FDL declaration order for private and announced types New Simplifier tactics for dealing with rational inequalities and Examiner generated proof rules User defined proof rules for the Simplifier New Checker rules for MODULAR expressions Significant performance improvement for Simplifier and Checker Release 7 31 April 2006 Release 7 31 of the toolset comprised Examiner version 7 31 Simplifier 2 24 Checker 2 07 Significant features of this release included Correction to
46. ombieScope files and enhanced POGS Output BOS Q 2 cesacs save toveshve cei davsdeeveceasdecsssshed vescavcess aaa a E ENAR EEEE 28 9 SPARKFormat changes sssssnsssssnnnnenennnunnnnnnnnnnnnnnnnnnnnnnnnnnnn nnna 29 9 1 Remove order declaration option J121 025 ssssessessessessssnnse 29 10 SPARKMake Changes sssssssnseenennnnnnnnnnnnnnnnnnnnnnnnnnnnnnnn nnmnnn 30 10 1 Language selection switch IA16 037 ssessesssesrresrrsrrsrrsernsrrnerneens 30 11 ZombieScope ChangeS sssssssennnunnnnennnnnnnnnnnnnnnnnnnnnnnn nnmnnn 31 11 1 Distribution of ZOMDICS COPE cece eeeeeeceeeeeeeeeeeaeeeseseeeseenteeeseeaeees 31 12 Backward incompatibilities c cccsssseeeeeesssseeeesseeeeeeees 32 12 1 Checker Replace_more prompt 1820 002 ce eeceeeeeeeeeeeseeees 32 12 2 Improved reasoning of false hypothesis 1820 003 32 12 3 Removal of rtc exp and realrtcs switches ICO1 020 32 12 4 Remove order declaration option in SPARKFormat J121 025 32 12 5 Enhanced management of Hypothesis Identifiers I629 007 32 13 User manual change SUMMALY c ssseseeeeeeceeeeeeeeeeneneeeeeeess 33 13 1 New Global Documentation INdEX eeeceeeeeseeeeeeeeeeseeeeeseeseeeeesseaees 33 13 2 SPARK Language Definitions eeceeeseseeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeee 33 13 3 Examiner User Manuals apanr ara ayaan Na iaa 33 13 4 Checker User Manual lsiscscissiess cossenv castensssasvouvs a 33 1
47. opment and Support RN attran PRAXIS SPARK Toolset Release Note 9 Issue 3 19 7 Proof Checker changes Proof Checker 9 0 0 includes the following changes and improvements 7 L New replace_more flag 1820 002 Added flag replace_more The flag determines if the user is prompted for more replacements after a replace command The default value is off For backward compatibility set the flag to on This can be done via the set command as described in the Proof Checker User Manual section 5 2 6 7 2 Improved reasoning of false hypothesis 1820 003 Added flag auto_infer_from_false When the flag is set to on then the done command will discharge a VC if one of the hypothesis is false The default value is on For backward compatibility set the flag to off This can be done via the set command as described in the Proof Checker User Manual section 5 2 6 Page 27 of 51 olT Ran C i Tool Development and Support RN 8 1 8 2 PRAXIS SPARK Toolset Release Note 9 Issue 3 19 POGS changes POGS 9 0 0 includes the following changes and improvements Preserve casing when reporting files used 1605 005 This change affects POGS on Windows platforms only Previously on Windows POGS would normalise the paths and filenames of all files to lower case in its output On other platforms it preserved the original casing This normalisation on Windows has now been removed so filename casing is preserved consistent
48. port SEPR or GNAT Tracker Ticket TN number is given 14 1 1 General The SPARK 95 language definition removes the distinction between initial and later declarative items this distinction remains in force in the Examiner that requires SPARK 83 declaration orders even in SPARK 95 mode SEPR 813 The Examiner does not yet permit the use of 8 bit characters in SPARK 95 user defined identifiers SEPR 818 Universal expressions in a modular context may sometimes require type qualification SEPR 1591 The Examiner does not yet permit the use of use type following an embedded package specification SEPR 747 The Examiner does not yet permit the renaming of packages in the same way that subprograms can be renamed SEPR 1391 The Examiner does not yet allow the Base attribute when not used as a prefix SEPR 1114 The Examiner does not yet allow S Range where S is scalar SEPR 1115 The use of a tagged view conversion as the target of an assignment is not implemented SEPR 2739 14 1 2 Verification Condition Generation and Run time Checks Ada string inequality and ordering operators are not modelled Their use can result in a the Simplifier reporting an FDL typecheck error The workaround is to wrap the operator concerned in a user defined function TN IC21 017 VCs involving string catenation that includes the character ASCII NUL will be incorrect SEPR 661 Aggregates of multi dimensional arrays cannot be modelled
49. semantically equivalent to the absence of an overriding indicator Note that the semantics for SPARK 2005 differ from Ada 2005 In Ada 2005 the absence of an overriding indicator means that the subprogram either overrides or not overrides an operation Page 7 of 51 olT Ran C i Tool Development and Support RN 2 2 2 3 2 4 PRAXIS SPARK Toolset Release Note 9 Issue 3 19 Checking safety and security policies using flow analysis IC15 003 Release 9 of the Examiner adds support for the checking of specific information flow policies using the Integrity property of an own variable to label the integrity of an input output or state variable These labels and policies for example allow the Examiner to enforce the rule that a Top Secret state or input should not affect an Unclassified state or output Two policies are predefined called security and safety these are decribed in section 8 3 of the Examiner User Manual Allow labels on statements in SPARK SEPR 2703 SPARK now permits statements to be labelled as in Ada for purposes such as instructing a debugger when to break For example procedure Increment X in out Integer derives X from X is T Integer not a statement so label not allowed begin lt lt gt T 1 lt lt L2 gt gt if X lt Integer Last then lt lt L3 gt gt X X T else label not permitted her lt lt L4
50. t revision to the rules regarding the placement of tagged type declarations e Correction to the modelling of Boolean type membership operators in the verification conditions e Support for generating VCs that allow the verification of the Liskov Substitution Principal LSP for tagged types and their operations e Dramatically improved performance of the Simplifier particularly in the simplification of quantified expressions Release 7 0 July 2003 Release 7 0 of the toolset comprised Examiner version 7 0 Simplifier version 2 12 Release 7 0 added e Ravenscar profile extensions to the language e Support for Ada Interrupts and Ada Real_Time in the configuration file e The new noduration command line switch e VC generation for unconstrained formal parameters e Suppression of VC generation for illegal function bodies e New SPARKFormat tool Release 7 2 December 2004 Release 7 2 of the toolset comprised Examiner version 7 2 Simplifier version 2 17 Page 43 of 51 olT Ran C f Tool Development and Support RN 15 12 PRAXIS SPARK Toolset Release Note 9 Issue 3 19 Release 7 2 added Unconstrained string constants to the language Instantiation of Unchecked_Conversion to the language Full record subtypes to the language Declaration of subprograms in the private part of packages Refined proof annotations for private types suffix for referring to value of variable on entry to loop in pro
51. uxindex then the unit will be found Page 15 of 51 arran Tool Development and Support RN 4 7 4 8 PRAXIS SPARK Toolset Release Note 9 Issue 3 19 in p a_aux idx If the required unit is P A D and this is not defined in either P auxindex or P A auxindex then the search will continue in the super index file Super idx The other difference in behaviour is in error handling and the issuing of warnings The Examiner will terminate immediately with an error message if an error is encountered in an index file It will issue a new warning Suppressible using the warning control file keyword index_manager_duplicates if two identical entries exist within the index file hierarchy There should be no noticeable change in behaviour using index files which satisfy the previous rules New switch to select language profile 1717 014 A new switch allows selection of the sequential language profile It takes the form language 83 95 2005 This switch replaces the existing ada83 switch which is now considered obsolete We recommend that all users upgrade their default switch files project files and scripts to use the new switch In combination with the profile switch this yields five legal language profiles sequential SPARK83 sequential SPARK95 sequential SPARK2005 RavenSPARK95 and RavenSPARK2005 Attempting to combine SPARK83 and RavenSPARK is illegal and is rejected by the Examiner Note currently SPARK2005 mode is

SPARK Toolset Release Note 9

Contents

Download Pdf Manuals

Related Search

Related Contents