Order of class invariant and routine pre-condition evaluation ? 
Author Message
 Order of class invariant and routine pre-condition evaluation ?

Quote:

> Thanks for answering my question so precisely - I ought to have been as
> precise in asking my question. What I'm really after is this ...

Maybe I can help, it's so simple to ask you compiler ... ;-))

Here is how to do so:
files: Ace, assert.e, client.e

-- Ace
system assert
root
    assert : make
default
    assertion (all)
cluster
   here: "."
   kernel: "../kernel"
end -- program assert

--assert.e
class ASSERT
creation
   make
feature
   c: CLIENT;
   make is
      do
         !!c;
         rout;
         c.rout;
      end
   rout is
      require req
      do
      ensure ens
      end
   req : BOOLEAN is
      do
         Result := True
         io.put_string ("require%N")
      end
   ens : BOOLEAN is
      do
         Result := True
         io.put_string ("ensure%N")
      end
   inv : BOOLEAN is
      do
         Result := True
         io.put_string ("invariant%N")
      end
invariant
   inv
end

-- client.e
class CLIENT
feature
   rout is
      require req
      do
      ensure ens
      end
   req : BOOLEAN is
      do
         Result := True
         io.put_string ("require-client%N")
      end
   ens : BOOLEAN is
      do
         Result := True
         io.put_string ("ensure-client%N")
      end
   inv : BOOLEAN is
      do
         Result := True
         io.put_string ("invariant-client%N")
      end
invariant
   inv
end

This is the output:
esclare> assert
invariant-client
require
ensure
require-client
ensure-client
invariant-client
esclare>

Details:
esclare> assert
invariant-client    -- end of creation of 'c'
require             -- call of 'rout'
ensure              -- no invariant since we are in creation routine
require-client      -- call to 'c.rout'
ensure-client
invariant-client    -- invariant checked after postcondition
esclare>

Hope this HELP ! (ps: my compiler is TowerEiffel)
--
Nicolas__

new version of STRUCTURE (2.5) available !

--
Nicolas__



Fri, 10 Apr 1998 03:00:00 GMT  
 Order of class invariant and routine pre-condition evaluation ?

Quote:

> Thanks for answering my question so precisely - I ought to have been as
> precise in asking my question. What I'm really after is this ...

Maybe I can help, it's so simple to ask you compiler ... ;-))

Here is how to do so:
files: Ace, assert.e, client.e

-- Ace
system assert
root
    assert : make
default
    assertion (all)
cluster
   here: "."
   kernel: "../kernel"
end -- program assert

--assert.e
class ASSERT
creation
   make
feature
   c: CLIENT;
   make is
      do
         !!c;
         rout;
         c.rout;
      end
   rout is
      require req
      do
      ensure ens
      end
   req : BOOLEAN is
      do
         Result := True
         io.put_string ("require%N")
      end
   ens : BOOLEAN is
      do
         Result := True
         io.put_string ("ensure%N")
      end
   inv : BOOLEAN is
      do
         Result := True
         io.put_string ("invariant%N")
      end
invariant
   inv
end

-- client.e
class CLIENT
feature
   rout is
      require req
      do
      ensure ens
      end
   req : BOOLEAN is
      do
         Result := True
         io.put_string ("require-client%N")
      end
   ens : BOOLEAN is
      do
         Result := True
         io.put_string ("ensure-client%N")
      end
   inv : BOOLEAN is
      do
         Result := True
         io.put_string ("invariant-client%N")
      end
invariant
   inv
end

This is the output:
esclare> assert
invariant-client
require
ensure
require-client
ensure-client
invariant-client
esclare>

Details:
esclare> assert
invariant-client    -- end of creation of 'c'
require             -- call of 'rout'
ensure              -- no invariant since we are in creation routine
require-client      -- call to 'c.rout'
ensure-client
invariant-client    -- invariant checked after postcondition
esclare>

Hope this HELP ! (ps: my compiler is TowerEiffel)
--
Nicolas__

new version of STRUCTURE (2.5) available !

--
Nicolas__



Fri, 10 Apr 1998 03:00:00 GMT  
 Order of class invariant and routine pre-condition evaluation ?

Extract from comp.lang.eiffel some days ago ;-):
(-- about order of interpretation of invariant, pre and post-conditions)

Quote:
> Thanks for answering my question so precisely - I ought to have been as
> precise in asking my question. What I'm really after is this ...

Maybe I can help, it's so simple to ask you compiler ... ;-))

Here is how to do so:
files: Ace, assert.e, client.e

-- Ace
system assert
root
    assert : make
default
    assertion (all)
cluster
   here: "."
   kernel: "../kernel"
end -- program assert

--assert.e
class ASSERT
creation
   make
feature
   c: CLIENT;
   make is
      do
         !!c;
         rout;
         c.rout;
      end
   rout is
      require req
      do
      ensure ens
      end
   req : BOOLEAN is
      do
         Result := True
         io.put_string ("require%N")
      end
   ens : BOOLEAN is
      do
         Result := True
         io.put_string ("ensure%N")
      end
   inv : BOOLEAN is
      do
         Result := True
         io.put_string ("invariant%N")
      end
invariant
   inv
end

-- client.e
class CLIENT
feature
   rout is
      require req
      do
      ensure ens
      end
   req : BOOLEAN is
      do
         Result := True
         io.put_string ("require-client%N")
      end
   ens : BOOLEAN is
      do
         Result := True
         io.put_string ("ensure-client%N")
      end
   inv : BOOLEAN is
      do
         Result := True
         io.put_string ("invariant-client%N")
      end
invariant
   inv
end

This is the output:
esclare> assert
invariant-client
require
ensure
require-client
ensure-client
invariant-client
esclare>

Details:
esclare> assert
invariant-client    -- end of creation of 'c'
require             -- call of 'rout'
ensure              -- no invariant since we are in creation routine
require-client      -- call to 'c.rout'
ensure-client
invariant-client    -- invariant checked after postcondition
esclare>

Hope this HELP ! (ps: my compiler is TowerEiffel)
--
Nicolas__



Sun, 12 Apr 1998 03:00:00 GMT  
 
 [ 3 post ] 

 Relevant Pages 

1. Order of class invariant and routine pre-condition evaluation ?

2. Order of class invariant and routine pre-condition evaluation ?

3. Order of evaluation of conditions in a combined condition

4. Order of evaluation of conditions in a combined condition/PMAP

5. Normal Order Evaluation Vs.Applicative Order Evaluation?

6. Pre-condition vs. Post-condition

7. Pre-condition vs. Post-condition

8. Pre-condition vs Post-condition

9. "BIG E vs little e", was pre-condition vs post-condition

10. pre-condition vs post-condition

11. Where to implement Pre and Post Conditions?

12. Eiffel quiz #1: Class invariant, non-atomic update of multiple objects

 

 
Powered by phpBB® Forum Software