Re: SPARK : third example for Roesetta - reviewers welcome

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

Le Mon, 16 Aug 2010 10:37:36 +0200, Phil Thornley  
<phil.jpthornley@gmail.com> a écrit:
> It appears to be very simple (although I haven't tried to do anything
> yet).  The entry for a language consists of blocks (of text in any
> format, although it does keyword colouring for known languages) that
> can be called 'source' interspersed with any other text that can
> explain the contents of the 'source' blocks.
>
> So there's no problem adding user rules, just the question of whether
> that is a good idea or not.
My personal opinion about user rules kept apart, my fear is that external  
files would make it look more like a tool than a language, or at least not  
as easy to track as any other language. Separation of spec and body in one  
common thing, adding a third file while examples show proofs can also  
appears in source as well, would be strange (sometime here, sometime  
there). Moreover, don't forget that SPARK and its annotation are a  
language, and Praxis Examiner/Simplifier are a particular implementation  
of SPARK. The only one at the time, I know, but still a particular  
implementation. User rules are by the way not even described in the SPARK  
LRM.

Just to compare, I did not saw any kind of external resource files at this  
wiki.

If at least if this could be located in the same directory as the  
source... but this have to be located at some place which depends on some  
SPARK configuration.