Change to the spec...missed a consistency property. Adding timing option.
[repair.git] / Repair / RepairCompiler / MCC / specs / abiword / abi.constraints
1 [], sizeof(firstblock)=1;
2 [], sizeof(Fragments)=1;
3 [], sizeof(secondblock)=1;
4 [forall f in Frags], (!(sizeof(f.Next)=1)) or ((f.Next.Prev=f) and sizeof(f.Next.Prev)=1);
5 [forall f in Frags], (sizeof(f.~Next)<=1);
6 [forall f in firstblock], sizeof(f.~Next)=0;
7 [forall l in Last, forall f in Fragments], f.PLast=l and sizeof(f.PLast)=1;
8 [forall f in Frags], f.Length>=1;