Method to add new operation(s) in a refinement

[zakiahzu...@gmail.com]

Hi,
I have read that b-method does not allowed to add a new operation in a refinement.
Is there any other way to add new operation in the refinement ? I have try to
create a machine that store the new operation and include it in the refinement.
But, still not successful. The example is as followed :

MACHINE
 calculator

VARIABLES
 value

INVARIANT
 value : NAT

INITIALISATION
 value := 0

OPERATIONS

 add(num) =
 PRE
  num : NAT
 THEN
  value := num + num
 END

END

MACHINE
 calculator_2
INCLUDES
 calculator
 
VARIABLES
 value_2

INVARIANT
 value_2 : NAT  

INITIALISATION

 value_2 := 0

OPERATIONS

 multiply(num,num2) =
 PRE
  num : NAT &
  num2 = value
 THEN
  value_2 := num2 * num
 END

END

REFINEMENT calculator_2_r
REFINES calculator_2

VARIABLES
 value_2

INITIALISATION
 value_2 := 0

OPERATIONS

 multiply(num,num2) =
 PRE
  num : NAT &
  num2 = value
 THEN
  value_2 := num2 * num*num
 END;

 add(num) =
 PRE
  num : NAT
 THEN
  value := num + num + num
 END

 END