Re: SPARK

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

Le Wed, 19 May 2010 10:09:33 +0200, Phil Thornley  
<phil.jpthornley@googlemail.com> a écrit:
> For example an inference rule will only be used if it *directly*
> proves a conclusion.
> Section 7.2.1: "In order for the Simplifier to be able to make use of
> the rule, it must find an instance of the rule by pattern-matching it
> against the current VC (for inference rules, this essentially means
> against the undischarged conclusions of the VC)"
Thanks for the detail Phil.

> * Except that, of course, the full source of the Simplifier is
> available, and there is nothing to stop you making changes to it!
Simon has tell about a limit in this area. I see another, which is the  
biggest to me : this would be a kind of forking, and a fork is not any  
more something common. This would be a valid way for my own use only,  
which could not be shared any more ; someone else could not check  
something from me using his/her own SPARK installation. I use to be  
interested is some specifications of some other languages of the like,  
which I've never found, and gave up with the idea (of the probably too  
much big work) to attempt to create one, for this exact reason : this  
would be specific to me, to what I use. In this area, it is mandatory to  
have standards, otherwise, this is not as much interesting.

This is not only about checking for validity, this is also about  
expressing why it is so to others in way hey can trust and read.