POGS User Manual

1 Overview

The Examiner can generate Verification Conditions (VCs), the proof of which show partial correctness, safety properties, or freedom from exceptions for SPARK programs. The Examiner can also generate dead path conjectures (DPCs) which are processed by the ZombieScope tool in order to detect dead paths in SPARK programs. The number of VCs and DPCs generated for any non-trivial SPARK program can be large, so management and monitoring of proof activities and dead path detection is important. Typically, an engineer might want to ask:

· How many VCs are there in total?

· How many VCs are there of each type arising from each subprogram?

· How many VCs are proved by each of the proof tools (Examiner, Simplifier, ViCToR, Checker, review file)?

· How many VCs were proved by the Simplifier with the aid of user-defined proof rules?

· How many VCs were proved with the experimental tool ViCToR?

· How many VCs are there still unproved?

· How many VCs have been proved to be False[1]?

· Which subprograms still have unproved VCs?

· How many subprograms generated DPCs?

· How many subprograms contain dead paths?

· How many dead paths were detected?

The Proof ObliGation Summariser tool (“POGS”) is designed to assist in answering these questions.

POGS is a stand-alone software tool that reads and understands the structure of the VC and DPC files and logs produced by the other SPARK tools, and reports of the status of proofs and dead path analyses in a human-readable form.

2 POGS and the SPARK Tools

2.1 Relationship with the SPARK tools

The verification condition (VC) files produced by the Examiner can be manipulated by the proof tools. VCs can be simplified by the Simplifier and the proof of VCs too complex for automatic proof by the Simplifier can be attempted using the Proof Checker. VCs can also be proven using ViCToR which translates them into SMTLib format and uses one of the various SMT Solvers. VCs not proved by the above techniques may be documented as proved by review. Figure 1 overleaf gives an overview of the relationship between these tools and the input and output files used to connect them; please note that ViCToR has been omitted from this picture as it is still considered to be an experimental feature.

The dead path conjecture (DPC) files produced by the Examiner can be analysed by ZombieScope to find dead paths in SPARK source code. For each DPC, ZombieScope reports whether a dead path has been detected. The relationship between ZombieScope files and the other SPARK tools are shown in Figure 2.

Figure 1: Relationship of SPARK Tools for Discharging VCs

Figure 2: Relationship of SPARK Tools for Detecting Dead Paths

3 Operating POGS

POGS is a command-line driven tool. The command line syntax is given below.

Command-line = “pogs [-d=input_directory] [-i] [-o=output_file] [-p] [-s] [-v]”

The command line switches for POGS are:

Option	Syntax	Default	Description
directory	-d=dir	current directory	Search for files to process in dir and its subdirectories.
ignore_dates	-i		Prevents checking of the date and time stamps of the VC, Simplified VC, DPC, SDP and Proof Log files.
output_file	-o=file	<cwd>.sum	Send results to specified output file.
plain_output	-p		Prevents release information, and file paths being output to the .sum file.
short_summary	-s		Prevents the per-subprogram analysis section (which contains summary information for each VC and DPC) being output to the .sum file.
version	-v		Output version information.

When run, POGS traverses the tree of subdirectories rooted at the current working directory or the directory specified with the –d switch, looking for instances of:

· Files containing Examiner-generated verification conditions. These files end with the extension “.vcg”.

· Files containing Examiner-generated dead path conjectures. These files end with the extension “.dpc”.

· Files containing Simplifier Logs. These files end with the extension “.slg”

· Files containing simplified VCs. These files end with the extension “.siv”

· Files containing VCs proven by ViCToR. These files end with the extension “.vct”

· Files containing ViCToR logs. These files end with the extension “.vlg”

· Files containing Checker Proof Logs. These files end with the extension “.plg”

· Files containing VCs proved by review. These files end with the extension “.prv”. The prefix of the names of these files must exactly match the prefix of the corresponding ".vcg" file and must be in lower-case.

· Files containing ZombieScope summary dead path files. These files end with the extension “.sdp”.

Any files that match these naming conventions are opened and read. From the content of these files, POGS determines if each VC has been proved (by the Examiner, Simplifier, with User Defined Proof Rules, Checker, ViCToR or Review), or if a VC remains unproven. It also determines which DPCs represent non-executable (dead) paths. POGS then produces a summary report file.

The “-d=directory” command line option causes POGS to search for files in the specified directory and its subdirectories. It will also write its summary output file to the specified directory unless this is overridden by the “-o” option. If “-d” is not specified then POGS will operate in the current working directory.

The “-i” command line option prevents POGS checking the date and time stamps given in the VC, Simplified VC, VLG, DPC, SDP and Proof Log files. This option has been added to accommodate the Examiner’s option “‑plain_output”, which eliminates the date and time stamps from the files it produces. This option should therefore be used in conjunction with the Examiner’s “-plain_output” option.

The “-o=file” command line option causes POGS to write its summary output to the specified file. The file will be written to the directory that POGS is working in (either the current working directory, or that specified via “-d”) unless an absolute path is provided. Note that if this option is used the output filename will be exactly as specified, i.e. POGS will not append the extension .sum to the name.

The “-p” command line option prevents POGS outputting release information, drive and non-relevant directory designation to the summary file. When this option is selected, directory separators will appear as “/” to assist with comparison of summary files produced on different operating systems. The date and time of the summary is also suppressed in this mode.

The “-s” command line option prevents POGS from producing the per-subprogram analysis section (which contains summary information for each VC and DPC, see section 3.1.2). Only the header, and totals sections are produced. This is useful on very large projects where the standard summary file can become very big.

The “-v” command line option causes POGS to print version information and terminate.

3.1 POGS Summary file structure and content

POGS produces a single output file whose file name is the name of the current working directory where POGS is invoked with the extension “.sum” (for “Summary”) unless this is overridden by the “-o” option described above.

The Summary File contains three distinct sections: a header section, a per-subprogram analysis, and a totals section. These sections are described in more detail below.

3.1.1 The Header Section

The header section contains the following information:

· A banner showing the POGS version and date;

· A statement of the directory in which POGS was invoked and the date and time of the analysis;

· A list of the options selected.

A typical header section is shown below:

-------------------------------------------------------------------------------

Semantic Analysis Summary

POGS Pro Edition, Version 9.0.0, Build Date 20100212, Build

-------------------------------------------------------------------------------

Summary of:

Verification Condition files (.vcg)

Simplified Verification Condition files (.siv)

Verification Condition discharged by ViCToR (.vct)

Proof Logs (.plg)

Dead Path Conjecture files (.dpc)

Summary Dead Path files (.sdp)

"status" column keys:

1st character:

'-' - No VC

'S' - No SIV

'U' - Undischarged

'E' - Proved by Examiner

'I' - Proved by Simplifier by Inference

'X' - Proved by Simplifier by Contradiction

'P' - Proved by Simplifier using User Defined Proof Rules

'V' - Proved by ViCToR

'C' - Proved by Checker

'R' - Proved by Review

'F' - VC is False

2nd character:

'-' - No DPC

'S' - No SDP

'U' - Unchecked

'D' - Dead path

'L' - Live path

in the directory:

D:\sparkdev\tests\apps\tis\95\latch

Summary produced: 04-FEB-2010 11:13:10.82

Ignore Dates option selected.

3.1.2 The per-subprogram analysis section

This section contains an analysis of the Verification Conditions and Dead Path Conjectures for each subprogram encountered. Note that the analysis of a subprogram will only appear in this section if the files associated with this subprogram were not detected as containing errors. Where shown, the analysis of each subprogram contains the following information:

· The VCG file from which the unsimplified VCs were read;

· The name of the corresponding subprogram;

· The date and time that the VCs were generated (if -i option is not selected);

· The date and time that the VCs were simplified (if the simplifier has been applied and if -i option is not selected);

· The date and time that the proof checker was last used on the simplified VCs (if the proof checker has been used);

· A list of any user-defined rules that were used, and the VCs for which they were used;

· The DPC file from which ZombieScope reads dead path conjectures;

· The date and time that the DPCs were generated (if -i option is not selected);

· The date and time that the DPCs were processed by ZombieScope;

· A table showing the detailed status of each VC/DPC in that subprogram.

Within a single subprogram, VCs and DPCs are numbered from 1.

The table shows the following information for each VC/DPC:

· Its number;

· The starting node of the VC/DPC in the subprogram’s flow graph. This can either be “start” (meaning the subprogram’s entry point where its precondition assertion is placed), or a line number which corresponds to an assert annotation in the subprogram’s source text, or blank in the case of a refinement VC.

· The final node of the VC/DPC in the subprogram’s flow graph. This can be one of

1 “assert @ L”, meaning the VC/DPC’s path is terminated by an assert annotation at line L of the subprogram source text;

2 “assert @ finish”, meaning the VC/DPC’s path terminates at the subprogram’s postcondition or return annotation.

3 “check stm @ L”, meaning that the VC/DPC’s path terminates at an explicit check statement at line L of the subprogram’s source text;

4 “rtc check @ L”, meaning that the VC/DPC’s path terminates at a check inserted by the Examiner to show the absence of a predefined exception (these are only generated if the Examiner was invoked with the -rtc or the -exp options);

5 “pre check @ L”, meaning that the VC/DPC’s path terminates at a check inserted by the Examiner to show the precondition of a called subprogram is met by a call at line L of the subprogram’s source text.

6 “refinement”, indicating a VC which has arisen from the use of refined, abstract own variables.

7 “inheritance”, indicating a VC which has arisen from the use of an inherited, overridden operation of a tagged type.

· The proof status of the VC. A VC can be exactly one of:

1 Proved by the Examiner, in which case the proof is recorded in the “.vcg” file.

2 Proved by the Simplifier, in which case the proof is recorded in the “.siv” file – the status shows if the Simplifier discharged the VC by an inference proof, proof by contradiction or proof using user defined rules.

3 Proved using ViCToR. The state of the proof is recorded in the “.vct” file. Although a log is contained in the “.vlg” file, this only lists incidents relating to the translation of VCs to SMTLib. Currently Alt-Ergo, the default SMT solver used, does not generate proof certificates.

4 Proved by the Checker, in which case the proof is recorded in the “.plg” file.

5 Proved by the review file, in which case the proof is recorded in the “.prv” file.

6 Proved by the Simplifier to have a false conclusion, in which case the VC is marked as “False”.

7 Unproved, in which case the VC is marked as “Undischarged”.

· The dead path status of the DPC. A DPC can be exactly one of:

1 Dead path has been detected by ZombieScope and this is recorded in the “.sdp” file.

2 Dead path has not been detected by ZombieScope and this is recorded in the “.sdp” file.

3 ZombieScope has not checked the DPC for dead path as the DPC is for an intermediate check – that is, dead path check is not required. This is recorded in both the “.dpc” and “.sdp” files.

· A status column that shows the proof and dead path statuses using a two character code. The first character shows the proof status while the second shows the dead path status. The status codes and their meaning are shown in the header of each POGS summary file – see Section 3.1.1.

An example of a per-subprogram summary is shown below. This subprogram generates three VCs. The first is a precondition check VC at line 77 of the source code. The second and third are the VCs associated with the path from F’s precondition to postcondition. We can see from the summary that the first VC was proved by the Simplifier, making use of a user-defined rule file, and the second VC was proved by the Checker and the third VC was discharged using ViCToR.

File D:\spark\basictypes\basictypes_full_plg\f.VCG

function BasicTypes.F

VCs generated 10-APR-2007 10:39:08

VCs simplified 10-APR-2007 10:53:33

The following user rules were used:

from function_f.rlu

rule(1) used in proving VCs:

VCs proved 10-APR-2007 13:33:45

VCs for function_f :

------------------------------------------------------------------------------

|-----------------------------------------------------------------------------

-----------------------------------------------------------------------------

If there are any VCs which appear in the review file but have already been proved elsewhere, there is only one entry in the table, and a warning is given. There is also a warning for any files which appear twice in the review file. For example:

*** Warning: VC 2 in proof review file has been proved by the simplifier ***

*** Warning: VC 3 in proof review file has been duplicated ***

3.1.3 The Totals Section

The final section of the POGS report has a number of subsections with each summarising facets that are related to the entire set of subprograms analysed.

First, if any of the .vcg, .slg, .siv, .vct, .vlg, .plg, .dpc and .sdp files contain errors, the names of the files containing the errors are listed preceded by a count of the errors detected. Further, if a .siv files exists, but does not have a corresponding .slg file, then the missing .slg file is also listed:

***WARNING: The following files, or their absence, raised warnings or errors:

1 d:\sparkdev\tests\simplifier\1981\95\vc_prob\a.siv

1 d:\sparkdev\tests\simplifier\1981\95\vc_prob\b.siv

1 d:\sparkdev\tests\simplifier\1981\95\vc_prob\c.siv

If any of the files associated with a subprogram are detected as containing errors, the analysis of the subprogram is aborted. No more files associated with the subprogram will be inspected. The summary results only describe subprograms that did not contain any errors. Instead, if non-zero, the number of subprograms with errors are highlighted in both the totals section and final total summary table.

Next, if any referenced user defined rule files contain syntax errors, the files containing the errant rules are listed:

***WARNING: The following user defined rule files contain syntax errors:

d:\sparkdev\tests\simplifier\seprs\2106\02\control\double_rotation.rlu

A list of any user defined rule files used is then presented:

The following user-defined rule files have been used:

d:\sparkdev\tests\simplifier\seprs\2106\02\control\double_rotation.rlu

d:\sparkdev\tests\simplifier\seprs\2106\02\control\control.rlu

If any VCs have been identified as False the subprograms containing these VCs are given next with each subprogram preceded by the number of False VCs contained within:

The following subprograms have VCs proved false:

1 d:\sparkdev\tests\simplifier\seprs\1688\omithyp\abs1.vcg

3 d:\sparkdev\tests\simplifier\seprs\1688\omithyp\abs2.vcg

4 d:\sparkdev\tests\simplifier\seprs\1688\omithyp\abs3.vcg

If subprograms exist which contain undischarged VCs (excluding VCs that have been proved False), these are listed next, each subprogram preceded by the number of undischarged VCs :

The following subprograms have undischarged VCs (excluding those proved false):

1 d:\sparkdev\tests\simplifier\1981\95\vc_prob\a.vcg

1 d:\sparkdev\tests\simplifier\1981\95\vc_prob\b.vcg

1 d:\sparkdev\tests\simplifier\1981\95\vc_prob\c.vcg

9 d:\sparkdev\tests\simplifier\seprs\1597\t.vcg

Similar lists for subprograms containing VCs proved by contradiction, subprograms that have VCs proved with the aid of user defined proof rules and subprograms that have VCs proved by the experimental ViCTOR tool follow. If there are no such VCs in the report these lists will not appear.

A summary of all the files containing VCs which have been duplicated in the review file is then given, along with a warning that this may indicate that the .prv file is out of date.

Next is a summary of the total use by subprogram of the different proof strategies:

Proof strategies used by subprograms

-------------------------------------------------------------------------

Total subprograms with at least one VC proved by examiner: 2

Total subprograms with at least one VC proved by simplifier: 15

Total subprograms with at least one VC proved by contradiction: 5

Total subprograms with at least one VC proved with user proof rule: 11

Total subprograms with at least one VC proved by ViCToR: 4

Total subprograms with at least one VC proved using checker: 7

Total subprograms with at least one VC discharged by review: 2

Following on is a summary of the proof strategies used for subprograms that are fully proven or discharged. The proof strategies are taken to have a hierarchy that is a measure of the extent of manual assistance required to prove a subprogram:

Examiner -> Simplifier -> User Defined Proof Rules -> ViCToR -> Checker -> Manual Review.

Subprograms proofs completed by strategies up to and including ViCToR are proved automatically, thereafter manual assistance is required up to the point where discharging a VC by review is entirely a manual process.

Where a subprogram is counted as, for example being proved by the simplifier or discharged by review, it will not be counted in preceding strategies of the hierarchy even if VCs proved by the preceding strategies form part of the overall proof of the subprogram. As an example:

Maximum extent of strategies used for fully proved subprograms:

-------------------------------------------------------------------------

Total subprograms with proof completed by examiner: 2

Total subprograms with proof completed by simplifier: 10

Total subprograms with proof completed with user defined rules: 2

Total subprograms with proof completed by ViCToR: 4

Total subprograms with proof completed by checker: 2

Total subprograms with VCs discharged by review: 2

Next is a summary of the overall status of the subprograms analysed:

Overall subprogram summary:

-------------------------------------------------------------------------

Total subprograms fully proved: 22

Total subprograms with at least one undischarged VC: 49 <<<

Total subprograms with at least one false VC: 2 <<<

-----

Total subprograms for which VCs have been generated: 73

If either the number of subprograms with at least one undischarged VC or the number of subprograms containing at least one False VC is non-zero, then the string “<<<” is appended to the corresponding line to draw attention to the total. Note that if a subprogram contains False VCs then it will only be counted in the total of subprograms with at least one False VC even if it has other VCs which are undischarged.

The sum of the subprograms fully proved plus the subprograms with at least one undischarged VC plus the subprograms with at least one False VC will always equal the total number of subprograms for which VCs have been generated. POGS includes an internal check for this invariant and POGS will fail with a fatal error should this invariant not be met.

Next is a summary of the analysis performed by ZombieScope. The file reports the number of subprograms that DPCs have been generated, the number of subprograms with dead paths and the total number of dead paths found.

ZombieScope Summary:

-------------------------------------------------------------------------

Total subprograms for which DPCs have been generated: 6

Total number subprograms with dead paths found: 1

Total number of dead paths found: 1

If any simplified subprograms have missing .slg files or if any of the files associated with a subprogram are detected as containing errors, these are listed in an error summary:

WARNING: Overall error summary:

-------------------------------------------------------------------------

Total simplified subprograms with missing slg file: 1

Total subprograms where analysis was abandoned due to errors: 13

The final table contains data on the total number of VCs of each type encountered by POGS for all subprograms, their proof status and a summary of the most important warnings and errors.

Total VCs by type:

-----------Proved By Or Using-----------

Total Spark Simp (User) ViCToR Checkr Review False Undisc

Assert/Post 285 0 111 16 14 11 0 133

Precondition 32 2 9 2 2 2 0 15

Check stmnt. 42 0 19 0 2 1 0 20

Runtime check 325 0 108 21 23 18 0 155

Refinem. VCs 2 0 0( 2) 0 0 0 0 0

Inherit. VCs 0 0 0 0 0 0 0 0

===============================================================================

Totals: 686 2 247( 2) 39 41 32 0 323 <<<

%Totals: <1% 36% <1% 6% 6% 5% 0% 47%

!!! WARNING: Experimental feature used: Proof by ViCToR

!!! ERRORS IN FILES RELATED TO ANALYSIS OF VCs; as below:

!!! Number of missing SLG (simplifier log) files: 62

!!! Number of erroneous VCG files: 1

!!! Number of erroneous SIV (simplified) files: 2

!!! Number of erroneous VCT (ViCToR) files: 2

!!! Number of erroneous VLG (ViCToR log) files: 3

!!! Number of erroneous PRV (manual proof review) files: 4

===================== End of Semantic Analysis Summary ========================

Here we see, for instance, that POGS encountered 325 runtime check VCs, none of which were proved by the Examiner, 108 of which have been proved by the Simplifier (0 using user-defined rules), 21 by ViCToR, 23 by the Checker, 18 by the review file with 155 remaining unproved. The totals for all columns are then presented in the “Totals” line at the bottom of the table. The totals as a percentage of the total number of VCs are also presented. Note that all listed percentages are approximate, rounded to the nearest whole integer. However, “0%” and “100%” always mean exactly 0% and 100% respectively. To offer greater precision, “<1%” means close to 0% (would have rounded down to 0%, but is not exactly 0%) and “>99%” means close to 100% (would have rounded up to 100%, but is not exactly 100%). Again, “<<<” is appended to the first total line to draw attention to any unproved or False VCs.

3.2 Errors and Warnings

The following subsections detail the warnings and errors that may be reported by POGS.

3.2.1 Warnings appearing in the POGS screen log

The following warnings are reported to the user as POGS is running, but do not cause POGS to terminate.

************* VC file corrupt: empty file ************

Issued when a VCG file is found but it contains zero data.

************* VC file corrupt: missing subprogram name ************

Issued when a VCG file is found but no subprogram name could be found inside the file.

************* VC file corrupt: no data beyond header ************

Issued when a VCG file is found but no data could be found beyond the header inside the file.

************* SIV file corrupt: empty file ************

Issued when a SIV file is found but it contains zero data.

************* SIV file corrupt: missing subprogram name ************

Issued when a SIV file is found but no subprogram name could be found inside the file.

************* SIV file corrupt: no data beyond header ************

Issued when a SIV file is found but no data could be found beyond the header inside the file.

************* Proof Log file empty ************

Issued when a PLG file is found but appears to contain no data.

Date format error in PLG file

Issued when the date-stamp in a PLG file cannot be understood.

Date format error in SIV file

Issued when the date-stamp in a SIV file cannot be understood.

*** Warning: VC file error: subprogram processing abandoned ***

Issued when an error in a VC file triggers the analysis of a subprogram to be aborted.

*** Warning: SIV file error: subprogram processing abandoned ***

Issued when an error in a SIV file triggers the analysis of a subprogram to be aborted.

*** Warning: SLG file error: subprogram processing abandoned ***

Issued when an error in a SLG file triggers the analysis of a subprogram to be aborted.

*** Warning: PLG file error: subprogram processing abandoned ***

Issued when an error in a PLG file triggers the analysis of a subprogram to be aborted.

*** Warning: PRV file error: subprogram processing abandoned ***

Issued when an error in a PRV file triggers the analysis of a subprogram to be aborted.

*** Warning: SDP file error: subprogram processing abandoned ***

Issued when an error in a SDP file triggers the analysis of a subprogram to be aborted.

************* DPC file corrupt: empty file ************

Issued when a DPC file is found but it contains no data.

************* DPC file corrupt: missing subprogram name ************

Issued when a DPC file is found but no subprogram name could be found inside the file.

************* DPC file corrupt: no data beyond header ************

Issued when a DPC file is found but no data could be found beyond the header inside the file.

************* SDP file corrupt: empty file ************

Issued when a SDP file is found but it contains no data.

************* SDP file corrupt: missing subprogram name ************

Issued when a SDP file is found but no subprogram name could be found inside the file.

************* SDP file corrupt: no data beyond header ************

Issued when a SDP file is found but no data could be found beyond the header inside the file.

************* ViCToR file corrupt: Could not parse line ************

*** Offending line was: [function_scale_movement_16,,,16,,true,0.05,,]

Issued when a particular line could not be parsed because it contains the wrong number of CSV entries. (In the above case, too many.)

*** Warning: VCT file error: ViCToR file corrupt: Could not parse line

Issued when any other parse error occurred.

*** Warning: VLG file error: Malformed timestamps

Issued when the timestamp contained in the vlg file is in the wrong format.

*** Warning: VLG file error: VCG file is newer than the VCT file

Issued if VCs have been re-generated and pogs encounters an outdated vct file.

*** Warning: VLG file error: SIV file is newer than the VCT file

Issued if SIV files have been re-generated and pogs encounters an outdated vct file.

*** Warning: VCT file error: Error raised by prover

Issued if victor raised an error during translation.

3.2.2 Errors appearing in the POGS screen log

The following errors are reported to the user as POGS is running, and cause POGS to immediately terminate. Such errors are usually due to corrupted and/or unexpected files being found in the tree below the current working directory. Any such errors should be reported to Altran Praxis.

Could not open expected input file - unexpected file system error

Issued when an input file (such as a VCG, SIV,PLG, DPC or SDP file) could not be opened for reading. This may be due to file protections, sharing, or some other operating-system dependent issue.

Could not open report file - check you have write permission for directory

Issued when the POGS Summary file cannot be created for writing. This may be due to file protections, sharing, or some other operating-system dependent issue.

Internal file table inconsistent.

Issued when a VC or DPC file cannot be found in POGS’ internal data structure.

Internal VC table inconsistent.

Issued when details of a particular VC or DPC cannot be found in POGS’ internal data structures. Can be caused by corruption and/or truncation of VCG, SIV, PLG, DPC or SDP files.

Expected directory not found.

Issued when a subdirectory cannot be opened.

Internal file table too small.

Issued when more than 80000 files are encountered. Contact Altran Praxis if this limit is insufficient.

Internal VC table too small.

Issued when more than 80000 VCs or DPCs are encountered in the same file. Contact Altran Praxis if this limit is insufficient.

Invalid command line

Issued when any command-line switch or argument is given.

Could not read from input file - unexpected file system error

Issued when an input file (such as a VCG, SIV, PLG, DPC or SDP file) could not be read. This may be due to file protections, sharing, or some other operating-system dependent issue.

Could not create temporary file

Issued when a temporary file used by POGS cannot be created. This may be due to file protections or some other operating-system dependent issue.

Overall subprogram summary counts inconsistent

Issued when the sum of the subprograms fully proved plus the subprograms with at least one undischarged VC plus the subprograms with at least one False VC does not equal the total number of subprograms for which VCs have been generated.

3.2.3 Errors appearing in the POGS Summary file

*** Error: The following line in the proof review file contains a syntax error: ***

*** <offending line>

Issued when a line in the proof review file does not match the syntax given in Appendix A. The line that contains the syntax error is output below the error message to help the user identify the problem.

3.2.4 Warnings appearing in the POGS Summary file

The following warnings appear in the POGS output summary file.

*** Warning: VC date stamps ignored ***

Issued when the -i (ignore date stamps) option has been selected. This implies the VC, Simplified VC, or Proof Log files may be out of date with each other.

*** Warning: DPC date stamps ignored ***

Issued when the -i (ignore date stamps) option has been selected. This implies the DPC, Summary DP files may be out of date with each other.

*** Warning: Simplified VC file out of date ***

Issued when the date-stamp in a SIV file is not more recent than the date-stamp in the corresponding VCG file. If POGS issues this warning, then the entire SIV file is assumed to be out-of-date, and its contents are ignored.

*** Warning: Simplified DPC file out of date ***

Issued when the date-stamp in a SDP file is not more recent than the date-stamp in the corresponding DPC file. If POGS issues this warning, then the entire SDP file is assumed to be out-of-date, and its contents are ignored.

*** Warning: Bad format in simplified VC file ***

Issued when a SIV file cannot be parsed by POGS. Usually due to corruption and/or truncation of the SIV file.

*** Warning: Proof Log file out of date *** (+Date stamps...)

Issued when the date-stamp in a PLG file is not more recent than the date-stamp in the corresponding SIV file. The offending date-stamps are also reported. If POGS issues this warning, then the entire PLG file is assumed to be out-of-date, and its contents are ignored.

*** Warning: VC x in the proof review file has been proved by the examiner ***

Issued when the examiner has proved a VC documented in the proof review file.

*** Warning: VC x in the proof review file has been proved by the simplifier ***

Issued when the simplifier has proved a VC documented in the proof review file.

*** Warning: VC x in the proof review file has been proved by the checker ***

Issued when the checker has proved a VC documented in the proof review file.

*** Warning: VC x in the proof review file is not recognised ***

Issued when the proof review file contains a VC number that is not present in the .vcg file.

*** Warning: VC x in the proof review file is duplicated ***

Issued when the proof review file contains multiple instances of the same VC number.

A Appendix: Grammar for .prv files

Proof review files have the following grammar:

PRVfile ::= {Line}

Line ::= [VCNumber][Comment]end_of_line_character

VCNumber ::= digit{digit}

Comment ::= --{non_end_of_line_character}

A.1 Example

For procedure DoIt we would have a file doit.prv as follows

-- .prv for procedure DoIt.

-- The following VCs were proved by review:

1 -- Proved by method x

3 -- Proved by method x

4 -- Proved by method y

7 -- Proved by method y

9 -- Proved by method y

10 -- Proved by method y

Document Control and References

Altran Praxis Limited, 20 Manvers Street, Bath BA1 1PX, UK.

File under

SVN: trunk/userdocs/Pogs_UM.doc (was S.P0468.73.71)

Changes history

Issue 0.1 (8th May 2000) First Draft for internal review.

Issue 1.0 (9th June 2000) First Definitive issue following review S.P0468.79.54.

Issue 1.1 (2nd February 2001) Definitive issue for POGS release 1.1. (NT and Solaris only)

Issue 1.2 (23rd August 2001) Definitive issue for POGS release 1.2.

Issue 1.3 (24th August 2001) Minor corrections after inspection.

Issue 1.4 (31st August 2001) Correct tools context diagram.

Issue 1.5 (5th November 2001) Updated after review S.P0468.79.74

Issue 1.6 (12 June 2002) Updated with proof review capability.

Issue 2.0 (13 June 2002) After review S.P0468.79.76

Issue 3.0 (30th September 2002) Update for POGS 3.0, supporting inheritance VCs

Issue 4.0 (16th April 2003): Updated to new template format.

Issue 5.0 (9 June 2003): Changes to new template, final format.

Issue 5.1 (10 June 2003): Final definitive issue following review.

Issue 5.2 (23 November 2004): Company name changed only.

Issue 5.3 (4 January 2005): Definitive issue following review S.P0468.79.88.

Issue 5.4 (3rd March 2005) Update for POGS 4.2, listing undischarged VCs

Issue 5.5 (31st March 2005) Changes to POGS to recognise false VCs and proof by contradiction

Issue 5.6 (17th October 2005) Updated for POGS 4.4 to accompany Examiner release 7.2d09.

Issue 5.7 (22nd November 2005): Changed Line Manager.

Issue 5.8 (1st December 2005): Updated following review S.P0468.79.90.

Issue 5.9 (9th May 2007): Updated to include x and s options.

Issue 5.10 (9th August 2007): Updated to reflect the changed subprogram summaries.

Issue 5.11 (14th August 2007): Allow Plain output and XML at the same time.

Issue 5.12 (11th February 2008): Improved error handling and reporting.

Issue 5.13 (3rd April 2008): Improved handling of percentages in summary table.

Issue 5.14 (11th July 2008): Updated following review S.P0468.79.93.

Issue 5.15 (26th August 2008): Made manual platform-independent.

Issue 5.16 (7th January 2009): Factored out contact details.

Issue 5.17 (12th January 2009): Documented new switches –d and –o.

Issue 5.18 (14th January 2009): Definitive issue following review.

Issue 5.20 (3rd February 2010): Rebrand for Altran Praxis Limited

Issue 5.21 (10th February 2010): POGS changes for ZombieScope and removed references to SPADE.

Issue 5.22 (24th February 2010): Changes to address review comments.

Issue 5.23 (4th October 2010): Fix typo in Section 3. [J910-024]

Issue 5.24 (12th October 2010): Correct references to the Examiner.

Issue 5.25 (2nd November 2010): Updated for SPARK Bridge / ViCToR integration.

Issue 5.26 (4th November 2010): Marked the –x option as deprecated.

Issue 5.27 (23rd September 2011): Removed the -x option.

Changes forecast

Further updates for SPARKBridge.

Document references

None.

[1] In POGS, A VC with at least one false conclusion is identified as a False VC. If it can be shown that this VC has contradictory hypotheses then the whole VC may yet be proved true. Thus, a False VC could either represent: A) An error - a mismatch between a program’s specification and its implementation or B) Not an error – a path that can never be executed.


		POGS POGS User Manual



		POGS/UM Issue: 5.27 Status: Definitive 23rd September 2011 Commercial In Confidence DOCTYPE:Praxis title:varchar=title reference:varchar=reference status:varchar=status issue:varchar=issue date:varchar=date projectname:varchar=DocumentSet Issue 5.27, Definitive, 23rd September 2011 000_000 POGS User Manual
		Originator
		SPARK Team
		Approver
		SPARK Team Line Manager