[SAL-HELP] axioms about a module

[Bruno Dutertre]

Angelo Gargantini wrote:
> I have the following (part of) spec:
> 
> cruisecontrol: CONTEXT =     BEGIN
>    main : MODULE = BEGIN
>        INPUT  ignited: BOOLEAN
>        INPUT  engRun: BOOLEAN
>    END;
>          % property for CC %%% replace with true
>    tp : THEOREM main |- G( true);
> END
> 
> I would like to add the assumption that when ignited is false, also 
> engRun is false, and then prove properties starting from that assumption.
> The only thing I can do now is to add a new BOOLEAN var and define:
> DEFINITION invCruise = ignited => NOT engRun
> And modify the theorem:
>    tp : THEOREM main |- G(invCruise => true);
> 
> Is there a way to add the assertion at the level of context?
> I tried to define a constant in the context (not in the module)
>    invCruise = main!ignited => NOT main!engRun
> but this is incorrect.
> I was not able to use "OBLIGATION" either, which may be useless, since 
> it is equivalent to THEOREM.
> My question: what is the right way to introduce an assumption about a 
> module and to use it when proving properties?
> thanks
> 
> Angelo Gargantini
> University of Bergamo  - Italy
> 
> 

Angelo,

You have to attach the assumption to a module as you sketched above. There's
no way to attach module properties to a context.

For simple assumptions there's no need to create a new variable,
you can just put it inside the temporal property. For example,
you can write

    tp: THEOREM main |- G((ignited => NOT engRun) => P)

For more complex assumptions, then adding a variable as you did above
may be the simplest approach.

If you don't want to modify the main module, then you can compose
it synchronously with a separate module that specifies the assumption.
For example, you can create a new module

   tester: MODULE =
     BEGIN
      INPUT ignited: BOOLEAN
      INPUT engRun: BOOLEAN
      OUTPUT invCruise: BOOLEAN
     DEFINITION
       invCruise = ignited => NOT engRUN
     END;

then rewrite the property as

    tp: THEORM (main || tester) |- G(invCruise => ..)


Bruno