Re: [Spark] Converting Arrays

["Phil Thornley" <phil.thornley@baesystems.com>]

"JP Thornley" <jpt@diphi.demon.co.uk> wrote in message
news:ON9GtiBcskb+IwAh@diphi.demon.co.uk...

> You can then write the proof rule for Length_Of_Path:
>     to_fullpath_rules(100): length_of_path may_be_replaced_by
>                             path__last - path__first + 1 .
>
> Append this to the generated rule file before running the Simplifier.
> (The rule number needs to be larger than the highest rule number
> generated by the Examiner).

Perhaps I should add that this is a slightly quick and dirty way of
getting the proof rule in. It has the advantage that the Simplifier will
be able to use it, but the disadvantage that the rule has to be created
for every subprogram that calls To_Fullpath as well as for To_Fullpath
itself (and I'm sure that no-one would ever contemplate creating a
different rule for different situations :-).

The more 'correct' way is to write a new rule family. Create a file
called (say) test.rls with contents:
   rule_family test:
      X requires [X:any].
   test_rule(1): length_of_path may_be_replaced_by
                            path__last - path__first + 1 .

(Warning - the above is as written, and unchecked.)

Then 'consult' this file in the Checker and use the rule in a 'replace'
command.

The advantage of this is that the rule is only written once, so there
can't be any mistakes made in duplicating it, but has the disadvantage
that the Simplifier won't be able to do anything with 'length_of_path'
and you end up with more VCs to prove in the Checker.

Cheers,

Phil

--
Phil Thornley
BAE SYSTEMS