spec module Atom {
    format P;
    format A; // contains an array of Ps.
              // but no interesting shape manipulation happens.
    default aInit(f, a) = f & (card(a)=1) & (a in Init);

    specvar Init, Predic, Correc:A set;
    
    proc init(a:A) suspends aInit
      requires card(a)=1 & (not (a in Init)) 
      modifies Init ensures a in Init';
    
    proc getM(a:A;idx:int) returns p:P ensures true; // ensures P in A
    
    proc clearAtom(a:A) calls Vec ensures true;
    
    // that's typestate, what about vcgen or something?
    proc predic(a:A;norder:int; coeffs:float[]) 
      modifies Predic, Correc calls Vec
      ensures (a in Predic') & not (a in Correc');
    proc correc(a:A; norder:int; coeffs:float[]) 
      requires (a in Predic) 
      modifies Predic, Correc calls Vec, C
      ensures (a in Correc') & not (a in Predic');
}