SPARK
in [ADA]
|
From: Yannick Duchêne (Hibou57) on 13 May 2010 17:43 Le Thu, 13 May 2010 22:05:05 +0200, Rod Chapman <roderick.chapman(a)googlemail.com> a écrit: > -debug=d dumps expression DAGS in DOT format. > > -debug=v or V produces output on the screen AND also produces > DOT format for the VCG graph(s) alongside the generated .vcg > files. if you use -debug=V and then look at the sequence of generated > graphs in numerical order, you'll see how the VC-generator works! Yes, was confused by previous runs which has left some .dot files in the place. The HTML output (-html) seems also recommended, as it produce even more handily browsable stuff than only relying on the Location pane of GPS. If this can ever be useful, here is a simple Windows script to generate all images for each dot files. For Windows users, you can then simply open any one image and watch all using the Windows image-slide capabilities. Doing so, you can quickly switch from one image to another, to see these like in a stroboscopic animation. rem ----- Graphs_To_Images.bat --------------------------- @echo off cls rem Set you input and input directory here. The Dot_Exe_Path variable rem is the path to your dot binary. If in the PATH, simply leave it as rem dot.exe. Input_Directory is the one you gave to the Examiner with its rem output_directory option. set Input_Directory=SPARK set Output_Directory=Graphs_Images set Dot_Exe_Path=dot.exe rem Ensure the output directory exists if not exist %Output_Directory% md %Output_Directory% rem Cleanup the content of the output directory to not have rem any previous images which would now be "garbages". del /Q %Output_Directory%\*.png del /Q %Output_Directory%\*.gif del /Q %Output_Directory%\*.svg rem For each .dot file in input directory, create a PNG image in output rem directory. The images names are after the ones of the .dot files. for %%f in (%Input_Directory%\*.dot) do %Dot_Exe_Path% -Tpng -o%Output_Directory%\%%~nf.png %%f rem Cleanup .dot files as well, to not have a cluttered directory (we may rem want to quickly find relevant .vcg and report files). del /Q %Input_Directory%\*.dot rem For safety, assign an empty strings to variables, as these are always rem global with Windows cmd/bat files. set Input_Directory= set Output_Directory= set Dot_Exe_Path= rem ----- End of file ------------------------------------ -- pragma Asset ? Is that true ? Waaww... great
From: Yannick Duchêne (Hibou57) on 13 May 2010 21:20 Hello, once again playing with checker and examiner, Within all the documentations installed with SPARK, there are some named SPARK_QRGn.pdf. The one SPARK_QRG1.pdf contains a summary of annotations to be used with the language. I wonder if this document is part of the language definition or, if not, if I'm missing some documentations somewhere. The reason of this doubt is, an example, the â--# assert ... ;â annotation which is documented in SPARK_QRG1, and in no other documentation I've read. I did not read all deeply at the time, and just had an overview of some. Anyway, I searched the âExaminer_UM.pdfâ, âSPARK95.pdfâ among others for â# assertâ in the text, and did not found any occurrence. I can see it only in âSPARK_QRG1.pdfâ. Is this file part of the language definition or did I missed some relevant documentation elsewhere ? -- pragma Asset ? Is that true ? Waaww... great
From: Yannick Duchêne (Hibou57) on 13 May 2010 23:07 The Quick Reference Card #1 talks about âtype assertionâ: > A type assertion allows the user to specify the base type which the > compiler will associate with a signed integer type. The base type > must be supplied to the Examiner in the configuration file. This > assertion allows the Examiner to generate VCs which are much more > readily discharged [RTC 5.2]. > > Example: > type T is range 1 .. 10 > --# assert TâBase is Short_Short_Integer; As the Examiner ignore any representation clauses [SPARK 95 (13.1)], it cannot care to any implicit representation clause either. So what's the purpose of this kind of assertions ? Does the examiner check something else which is not only the range ? Does it have something to deal with type conversions ? -- pragma Asset ? Is that true ? Waaww... great
From: Yannick Duchêne (Hibou57) on 13 May 2010 23:26 Suspected error. Unless I'm wrong for some reason, it seems the Quick Reference Card #1 contains an error. About âreturn annotationâ, it give the following exemple: function Max(X, Y: Integer) return Integer; --# return M => (A >= B -> M = X) and --# (B >= A -> M = Y); What're A and B if they aren't X and Y ? -- pragma Asset ? Is that true ? Waaww... great
From: Yannick Duchêne (Hibou57) on 14 May 2010 00:15
> The reason of this doubt is, an example, the â--# assert ... ;â > annotation which is documented in SPARK_QRG1, and in no other > documentation I've read. I did not read all deeply at the time, and just > had an overview of some. Anyway, I searched the âExaminer_UM.pdfâ, > âSPARK95.pdfâ among others for â# assertâ in the text, and did not found > any occurrence. I can see it only in âSPARK_QRG1.pdfâ. > > Is this file part of the language definition or did I missed some > relevant documentation elsewhere ? Found : it is detailed in the file Examiner_GenVCs.pdf (Generation of VCs for SPARK Programs) -- pragma Asset ? Is that true ? Waaww... great |