spec module Skratch_pad {
    format P;
    format Pad;

    specvar Init, Read, Updated:Pad set;
    default pInit(f, p) = f & (p in Init) & card(p) = 1;

    proc init(p:Pad) suspends pInit requires (not (p in Init)) & card(p) = 1
      modifies Init ensures p in Init';

    proc storeVM(p:Pad;v:P)
      calls Vec ensures true;
    proc storeH1pos(p:Pad;v:P)
      calls Vec ensures true;
    proc storeOpos(p:Pad;v:P)
      calls Vec ensures true;
    proc storeH2pos(p:Pad;v:P)
      calls Vec ensures true;
    proc storeH1force(p:Pad;v:P)
      calls Vec ensures true;
    proc storeOforce(p:Pad;v:P)
      calls Vec ensures true;
    proc storeH2force(p:Pad;v:P)
      calls Vec ensures true;

    proc getH1pos(p:Pad) returns rv:P requires p in Read 
      calls Vec ensures true;
    proc getOpos(p:Pad) returns rv:P  requires p in Read 
      calls Vec ensures true;
    proc getH2pos(p:Pad) returns rv:P requires p in Read 
      calls Vec ensures true;
    proc getVM(p:Pad) returns rv:P    requires p in Read 
      calls Vec ensures true;

    proc update_forces(p:Pad;Res:P[]) requires p in Read
      modifies Updated calls Vec ensures p in Updated';

    proc read_data(p:Pad;m:Molecule) 
      requires (m in H2O.Init) & card(m) = 1
      modifies Read, Updated, H2O.Pos, H2O.Vel
      calls Vec, H2O ensures (p in Read') & not (p in Updated');
}