Help sought for formal specification

[ct2049]

I've recently been handed a Object-Z specification for a (small)
application a and told I need to program it. I've always wanted to 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.




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

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/

[Colin LeMahieu]

I don't think that specific thing exists, but using start/off/forth
with item_for_iteration should get you there with a subclass.

--- In eiffel_software@..., "ct2049" <CT2049@...> wrote:

>
> I've recently been handed a Object-Z specification for a (small)
> application a and told I need to program it. I've always wanted to 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.
>

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

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/

[Bertrand Meyer]

I think you want MML:

 

                http://se.inf.ethz.ch/people/schoeller/mml.html

 

-- BM

 

From: eiffel_software@...
[mailto:eiffel_software@...] On Behalf Of ct2049
Sent: 24 April, 2008 05:22
To: eiffel_software@...
Subject: [eiffel_software] Help sought for formal specification

 

I've recently been handed a Object-Z specification for a (small)
application a and told I need to program it. I've always wanted to 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/

[ct2049]

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:

>
> I think you want MML:
>
>  
>
>                 http://se.inf.ethz.ch/people/schoeller/mml.html
>
>  
>
> -- BM
>
>  
>
> From: eiffel_software@...
> [mailto:eiffel_software@...] On Behalf Of ct2049
> Sent: 24 April, 2008 05:22
> To: eiffel_software@...
> Subject: [eiffel_software] Help sought for formal specification
>
>  
>
> I've recently been handed a Object-Z specification for a (small)
> application a and told I need to program it. I've always wanted to

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/

[Peter Gummer-2]

ct2049 wrote:

> 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?

A PREDICATE is instantiated as an agent for a BOOLEAN function. So you would
write a function like this:

>    is_less_than_100 (x: REAL): BOOLEAN
>            -- Is `x' < 100?
>        do
>            Result := x < 100
>        end

I am not familiar with MML_SET, but I assume you would do something like
this:

>    test.for_fall (agent is_less_than_100)

- Peter Gummer



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

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/