Re: Silly and stupid post-condition or not ?

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

Le Mon, 06 Feb 2012 15:39:14 +0100, Robert A Duff  
<bobduff@shell01.theworld.com> a écrit:

> "Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr> writes:
>
>> Seems nice, but given this…
>>
>>    subtype Image_Type is String
>>       with Static_Predicate => Image_Type'Length in Length_Type;
>>
>>    function Image (Instance : Instance_Type) return Image_Type
>>       with Post =>
>>         (Parsed (Image'Result).Status = Parsed) and
>>         (Parsed (Image'Result).Instance = Instance);
>>       -- Result can always be successfully parsed and the resulting
>>       -- instance is always equal to the one whose image is returned.
>>
>> …how do I move Image's Post predicate to an Image_Type's dynamic
>> predicate  ? I could not figure the syntax nor if it's at least  
>> possible.
>
> Not possible.  Predicates can only express a property of a single
> thing, but here you're trying to express a relationship
> between two things (parameter and result).
>
> - Bob


Sorry, my wording was unclear. Here is what I wanted, and it works:

    subtype Image_Type is String
       with Dynamic_Predicate =>
         (Image_Type'Length in Length_Type) and
         (Parsed (Image_Type).Status = Parsed);

(don't know why it first failed, may be a syntax error)

The predicate “Parsed (Image_Type).Status = Parsed” is better on  
Image_Type than on Image.

So thanks for your prior message which gave me this idea. Since now, will  
better think about moving predicates on types as much as possible. Indeed  
better.


-- 
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University