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

["Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>]

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.