Re: Help sought for formal specification

Thank you MML really seems to be what I need.
I am still running into one problem though, I need to add an
invariant that does a "for all" assertion on a set.  I thought I'd be
able to make a boolean query that would loop over the set and check a
condition. However, I don't see anything in the MML_SET that would
allow me to write my own loop.  
I noticed that MML_SET  has a feature called "for_fall" that takes a
predicate.  I think this may be what I want. However, it takes a
"PREDICATE" as a parameter and I'm having a lot of trouble
understanding how the PREDICATE class works and what I need to do to
set it up.

If I had some code that looks like this:
test : MML_SET[REAL]
and I'd like to make sure that every element in test is less than 100
how would I do this?

--- In eiffel_software@..., "Bertrand
Meyer" <Bertrand.Meyer@...> wrote: use
> Eiffel and this seemed like the perfect applicable to cut my teeth
on.
>
> I'm running into one problem in that the specification uses map
> modeling (or more specifically partial functions). It seems like
the
> hash table class would be the best choice for this, except it
doesn't
> have any features for range subtraction, which essentially is a
remove
> were you pass it an item and it removes all the keys associated
with
> that item.
>
> Now, I'm suppose to follow this specification as closely as
possible,
> is there any other Eiffel classes I should be looking at? Or should
I
> make my own class that inherits from the hash table and implements
> these missing features.
>
>  
>
>
>
> [Non-text portions of this message have been removed]
>



------------------------------------

Yahoo! Groups Links

<*> To visit your group on the web, go to:
    http://groups.yahoo.com/group/eiffel_software/

<*> Your email settings:
    Individual Email | Traditional

<*> To change settings online go to:
    http://groups.yahoo.com/group/eiffel_software/join
    (Yahoo! ID required)

<*> To change settings via email:
    mailto:eiffel_software-digest@...
    mailto:eiffel_software-fullfeatured@...

<*> To unsubscribe from this group, send an email to:
    eiffel_software-unsubscribe@...

<*> Your use of Yahoo! Groups is subject to:
    http://docs.yahoo.com/info/terms/