spec module Simparm {
    specvar Init : bool;
    specvar ParmsLoaded : bool;

    default I = Init;
    default PL = ParmsLoaded;

    proc max(f1:float; f2:float) returns rv:float suspends PL ensures true;
    proc sqr(f:float) returns rv:float suspends PL ensures true;

    proc init() suspends I, PL
      modifies Init ensures Init';
    proc loadParms(name:string) suspends PL
      modifies ParmsLoaded ensures ParmsLoaded';
    proc CNSTNT() suspends PL calls C ensures true;
    proc SYSCNS() suspends PL calls C ensures true;

    proc computeFAC() returns rv:float calls C ensures true;
    proc getCUTOFF() returns rv:float ensures true;
    proc getCUT2() returns rv:float ensures true;
    proc getBOXL() returns rv:float ensures true;
    proc getBOXH() returns rv:float ensures true;
    proc getFKIN() returns rv:float ensures true;
    proc getFHM() returns rv:float ensures true;
    proc getFOM() returns rv:float ensures true;
    proc getFPOT() returns rv:float ensures true;
    proc getELPST() returns rv:float ensures true;
    proc getIRST() returns rv:int ensures true;
    proc getNMOL() returns rv:int ensures true;
    proc getNORDER() returns rv:int ensures true;
    proc getNPRINT() returns rv:int ensures true;
    proc getNSAVE() returns rv:int ensures true;
    proc getNSTEP() returns rv:int ensures true;
    proc getREF1() returns rv:float ensures true;
    proc getREF2() returns rv:float ensures true;
    proc getREF4() returns rv:float ensures true;
    proc getTEMP() returns rv:float ensures true;
    proc getTLC() returns rv:float[] ensures true;
    proc getPCC() returns rv:float[] ensures true;
    proc setNFMC(v:int) ensures true;
    proc resetStat() ensures true;
}