SPARK POGS: List the rules used by the Simplifier

SPARK POGS: List the rules used by the Simplifier

[Phil Thornley]

The POGS tool in the SPARK GPL toolset summarises the state of the
proofs for a program.  But it is not easy to determine which user
rules have/have not been used by the Simplifier.

I have made a modified POGS that lists the rules used by the
Simplifier as part of the summary output so, instead of just the list
of rule files, it prints the following:

D:\SPARK\ordered_list2\ordered_lists\ordered_lists.rlu
  ordered_user(1)    ordered_user(6)    ordered_user(10)
  ordered_user(2)    ordered_user(7)    ordered_user(11)
  ordered_user(3)    ordered_user(8)    ordered_user(12)
  ordered_user(4)    ordered_user(9)    ordered_user(13)
  ordered_user(5)

D:\SPARK\ordered_list2\ordered_lists\delete.rlu
  delete_user(1)
  delete_user(2)

D:\SPARK\ordered_list2\ordered_lists\initialize.rlu
  init_user(1)   init_user(4)   init_user(7)
  init_user(2)   init_user(5)   init_user(8)
  init_user(3)   init_user(6)   init_user(9)

http://www.sparksure.com/resources/POGSRuleList.zip is an archive with
the new and modified files as well as a Windows executable.

http://www.sparksure.com/resources/pogsrulelist.patch is a patch file
(created by git).

Cheers,

Phil

Re: SPARK POGS: List the rules used by the Simplifier

[Yannick Duchêne (Hibou57)]

Le Fri, 13 Aug 2010 19:21:16 +0200, Phil Thornley  
<phil.jpthornley@gmail.com> a écrit:
> I have made a modified POGS that lists the rules used by the
> Simplifier as part of the summary output so, instead of just the list
> of rule files, it prints the following:
> [...]
So this report the kind of things which is otherwise split through  
multiple *.rls files ?

Re: SPARK POGS: List the rules used by the Simplifier

[Phil Thornley]

On 13 Aug, 18:52, Yannick Duchêne (Hibou57) <yannick_duch...@yahoo.fr>
wrote:

> So this report the kind of things which is otherwise split through  
> multiple *.rls files ?

No - *.rls files are produced by the Examiner, so it doesn't really
matter which of the rules in these files are used (in fact most of
them are not used).

These summaries are of the user rules - in *.rlu files - which are
hand coded and so have to be reviewed and maintained as the code
develops.  It's useful to be able to keep these rules to a minimum to
keep the maintenance load down.

(And, for example, one of the changes with SPARK 2010 will remove the
need for user rules for function return annotations, so these
summaries will help to identify which those rules are.)

In fact this information is already in the POGS summary - but it is
given for each operation, ahead of the table showing each VC in the
operation, and the way that it is presented makes it tedious to
identify which rules have/have not been used - particularly for
'package' rule files that might be used by a number of different
operations.

Cheers,

Phil

Re: SPARK POGS: List the rules used by the Simplifier

[Yannick Duchêne (Hibou57)]

Le Fri, 13 Aug 2010 21:04:00 +0200, Phil Thornley  
<phil.jpthornley@gmail.com> a écrit:
> No - *.rls files are produced by the Examiner, so it doesn't really
> matter which of the rules in these files are used (in fact most of
> them are not used).
>
> These summaries are of the user rules - in *.rlu files - which are
> hand coded and so have to be reviewed and maintained as the code
> develops.  It's useful to be able to keep these rules to a minimum to
> keep the maintenance load down.

Oops, so this can be seen as an extraction of some of the reports which  
belongs to *.slg files ? (the ones where steps of proof are exposed, like  
“Applied substitution rule multiply_rules(3)” and etc). Please, don't kick  
if I'm still wrong.

> (And, for example, one of the changes with SPARK 2010 will remove the
> need for user rules for function return annotations, so these
> summaries will help to identify which those rules are.)
Will see (I am not aware of these change so far).

> In fact this information is already in the POGS summary - but it is
> given for each operation, ahead of the table showing each VC in the
> operation, and the way that it is presented makes it tedious to
> identify which rules have/have not been used - particularly for
> 'package' rule files that might be used by a number of different
> operations.
OK (I don't use POGS so much, I mostly read *.siv files... and I am not  
using SPARK every day)

By the way, if you want to join, I am to open a new thread about “SPARK  
understand me very well... me neither” :D


-- 
There is even better than a pragma Assert: a SPARK --# check.
--# check C and WhoKnowWhat and YouKnowWho;
--# assert Ada;
--  i.e. forget about previous premises which leads to conclusion
--  and start with new conclusion as premise.