ensure 
Author Message
 ensure

Font:
class CAIXA
--
-- Programa "CAIXA"  
--
-- require_check
--
-- Para compilar:
-- compile -all_check caixa
-- compile -no_check caixa
--

creation {ANY}
   make

feature {ANY}

   total: DOUBLE;

   troco: DOUBLE;

   make is
      local
         preco: DOUBLE;
      do  
         io.put_string("Caixa%N");
         io.put_string("********************%N");
         from
         until
            preco = - 111.0
         loop
            io.put_string("$ ");
            io.read_double;
            preco := io.last_double;
            if preco /= - 111.0 then
               registre(preco);
            end;
         end;
         io.put_string("Total: ");
         io.put_double(total);
         io.put_new_line;
         io.put_string("Valor Pago: ");
         io.read_double;
         receba(io.last_real);
         io.put_string("Troco: ");
         io.put_double(troco);
         io.put_new_line;
         io.put_string("********************%N");
      end -- make

   registre(valor: DOUBLE) is
      require
         valor_negativo: valor >= 0;
      do  
         total := total + valor;
      ensure
         registre: total = old total + valor;
      end -- registre

   receba(valor_pg: DOUBLE) is
      require
         valor_pg_mq_total: valor_pg >= total;
      do  
         troco := valor_pg - total;
      ensure
         receba: troco = valor_pg - total;
      end -- receba

invariant

   troco >= 0;

   total >= 0;

end -- class CAIXA

Imput:
4.5
3.4

Error:
*** Error at Run Time ***: Ensure Assertion Violated.
*** Error at Run Time ***: registre
3 frames in current stack.
=====  Bottom of run-time stack  =====
System root.
Current = CAIXA#0x8060140
        [ total = 7.900000
          troco = 0.000000
        ]
line 21 column 4 file ./caixa.e
======================================
make CAIXA
Current = CAIXA#0x8060140
        [ total = 7.900000
          troco = 0.000000
        ]
preco = 3.400000
line 35 column 16 file ./caixa.e
======================================
registre CAIXA
Current = CAIXA#0x8060140
        [ total = 7.900000
          troco = 0.000000
        ]
valor = 3.400000
old l56c32CAIXA = 4.500000
line 56 column 26 file ./caixa.e
=====   Top of run-time stack    =====
*** Error at Run Time ***: Ensure Assertion Violated.
*** Error at Run Time ***: registre



Sat, 06 Mar 2004 06:45:01 GMT  
 ensure


Quote:

>   registre(valor: DOUBLE) is
>      require
>         valor_negativo: valor >= 0;
>      do  
>         total := total + valor;
>      ensure
>         registre: total = old total + valor;
>      end -- registre

I would always be weary of equations involving DOUBLEs, because
of rounding errors.  However, this particular one looks benign.

I wonder if some sort of truncation to FLOAT is happening internally?
Do you still get the same error of you change all the DOUBLEs to
FLOATs?

--
--
Patrick Doyle



Wed, 10 Mar 2004 10:19:00 GMT  
 ensure

Are you running on an Intel platform?

Such seemingly innocuous FP operations fail because pentiums compute
FP temporaries at 80 bits of precision. Therefore, this statement:
        registre: total = old total + valor;

is truncated to 64 bits on the left and then promoted to 80 bits,
while the right is computed at the full 80 bits.

The only way I got around this was to wrap FP comparisons with a
feature: about_equal (val1, val2: DOUBLE): BOOLEAN

which checks if val1 and val2 are equal within a `Tolerance' (for me,
about 1e-6).

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

Raytheon Systems Company                        (410)278-9149
Scientific Visualization Specialist
U.S. Army Research Laboratory   -   HPC Major Shared Resource Center
----------------------------------------------------------------------



Sat, 13 Mar 2004 00:47:16 GMT  
 
 [ 3 post ] 

 Relevant Pages 

1. ensure: vs valueOnUnwindDo: (bug in VW7 Web Toolkit?)

2. question on return from blocks and ensure: blocks

3. ENSURE statement in DOS

4. VA return from #ensure:

5. Ensuring Dylan Success

6. Difference between require and ensure just syntactic sugar?

7. does SE check ensure and invariant by default?

8. Method : what to ensure after creation ?

9. redefining require and ensure clauses

10. Return from ensure

11. require, ensure, and Design by Contract

12. A tool to ensure Software Quality

 

 
Powered by phpBB® Forum Software