[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Specification gen-execute
enrich gen-commands , 
       gen-sys-out , 
       gen-secdomain
 with
   functions 
      exec : systemstate × command → systemstateandoutput;
      comment: combines Rushby's step and output functions (def. 1);
       
      cdom : systemstate × command → secdomain;
      comment: Rushby's dom : A -> D;
       
      cdom : command → secdomain;
end enrich