[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,

Theorem base summary for Specification PLIB-preds

allReadsOK-def(0,0)allWritesOKInd-recW(0,0)allwritesOK-ind-add-write(19,6)at-overwrite-no-write(17,4)hist-more-persisted-append(6,2)overwrite-attach-read(10,3)persistDependentReads-otherread(0,0)restrict-R(0,0)restrict-l-W-other(2,0)restrict-t-one(2,0)
allReadsOK-firstreadpersisted(2,0)allreadsOK-filter-persisted(2,1)allwritesOK-ind-at-most-one-write(28,5)event-persistDependentReads(25,5)hist-more-persisted-base1(0,0)overwrite-attach-write(11,1)persistDependentReads-otherwrite(0,0)restrict-R-empty(2,0)restrict-l-W-same(2,0)restrict-thread(0,0)
allReadsOK-ind-no-initial-unpersisted-read(21,3)allreadsOK-ind-filter-persisted(18,3)allwritesOK-ind-one(6,3)events-append(2,0)hist-more-persisted-base2(0,0)overwrite-base(0,0)persistDependentReads-read(0,0)restrict-W(0,0)restrict-l-append(2,0)restrict-true-attach-false(2,0)
allReadsOK-no-initial-unpersisted-read(3,2)allreadsOK-ind-filter-persisted-upd-false(25,7)allwritesOK-ind-one-unpersisted-write-no-persisted-after(32,7)events-empty(2,0)hist-more-persisted-persistDependetReads(16,5)overwrite-one-read(2,1)persistDependentReads-restrict-empty(26,1)restrict-W-append(2,0)restrict-l-b-swap(3,1)restrict-true-attach-true(2,0)
allReadsOK-nowrites-allpersisted(3,2)allreadsok-add-read(3,1)allwritesOK-ind-pending-not-in(6,2)events-one(2,0)hist-more-persisted-rec(0,0)overwrite-one-write(2,1)persistDependentReads-restrict-other-loc(25,5)restrict-W-empty(2,0)restrict-l-empty(2,0)restrict-true-false(2,0)
allReadsOK-nowrites-allpersisted-ind(19,6)allreadsok-add-write(2,0)allwritesOK-ind-pending-zero-write(15,2)first-vol-write-head-restricted(24,3)hist-more-persisted-refl(2,1)overwrite-persist-dependent-reads(26,8)persistDependentReads-restrict-same-loc(17,3)restrict-b-append(2,0)restrict-l-one(2,0)restrict-true-false-empty(7,1)
allReadsOK-one(4,2)allreadsok-ind-add-read(11,3)allwritesOK-ind-persist-dependent-reads(26,8)first-vol-write-rec-read(4,3)hist-more-persisted-size-eq(11,2)overwrite-persist-dependent-reads-restrict-true(41,10)persistDependentReads-restrict-single-W(30,1)restrict-b-empty(2,0)restrict-l-t-swap(3,1)restrict-true-true(2,0)
allReadsOK-tailread(2,0)allreadsok-ind-add-write(11,1)allwritesOK-ind-persist-one-write(16,4)first-vol-write-rec-write-other(4,3)hist-more-persisted-trans(16,3)overwrite-persist-one-write(10,3)persisted-update-same(2,1)restrict-b-idem(11,1)restrict-loc(0,0)restrict-vp(0,0)
allReadsOKInd-base(0,0)allreadsok-ind-one(6,3)allwritesOK-ind-swap-flags-persist-one-write(21,10)first-vol-write-rec-write-persisted(4,3)lastPersisted-false-ex-persisted-write(22,7)overwrite-persist-one-write-restrict-true(56,8)persisted-update-swap(4,1)restrict-bool-one(2,0)restrict-read-R(2,0)restrict-w-b-swap(3,1)
allReadsOKInd-recR(0,0)allreadsok-ind-persist(31,14)allwritesOK-ind-swap-to-non-pending(12,5)first-vol-write-rec-write-unpersisted(3,2)lastPersistedOrElse-base(0,0)overwrite-rec-read(0,0)rely-attach(6,2)restrict-events(0,0)restrict-read-W(2,0)restrict-w-l-swap(3,1)
allReadsOKInd-recW(0,0)allreadsok-persist(2,0)allwritesOK-ind-unpersisted-one-write(10,4)first-vol-write-size(30,14)lastPersistedOrElse-recR(0,0)overwrite-rec-write(0,0)rely-def(0,0)restrict-false-attach-false(2,0)restrict-read-attach-W(2,0)restrict-w-t-swap(3,1)
allWritesOK-def(0,0)allwritesOK-add-read(2,0)allwritesOK-one(5,3)first-vol-write-size2(8,6)lastPersistedOrElse-recW(0,0)pending-update-same(2,1)rely-persist(3,1)restrict-false-attach-true(2,0)restrict-read-one(10,2)restrict-write-R(2,0)
allWritesOK-ind-filter-persisted(18,3)allwritesOK-add-write(3,1)allwritesOK-one-unpersisted-write-no-persisted-after(3,1)first-vol-write-size3(2,1)lastwrite-to-update(21,10)pending-update-swap(4,1)rely-refl(3,1)restrict-false-false(2,0)restrict-t-append(2,0)restrict-write-W(2,0)
allWritesOK-ind-filter-persisted-upd-true(18,6)allwritesOK-at-most-one-write(3,2)allwritesOK-persist-dependent-reads(2,0)first-vol-write-split(39,16)mem-update-same(2,1)persist-dependent-reads-unchanged-writes(24,5)rely-stable-write-empty(19,3)restrict-false-true(2,0)restrict-t-b-empty-expand-loc(17,5)restrict-write-attach-R(2,0)
allWritesOKInd-base(0,0)allwritesOK-filter-persisted(2,0)allwritesOK-persist-one-write(3,1)firstVolWrite-def(0,0)mem-update-swap(4,1)persistDependentReads-base(0,0)rely-stable-write-one(21,5)restrict-l-R-other(2,0)restrict-t-b-swap(3,1)restrict-write-one(2,0)
allWritesOKInd-recR(0,0)allwritesOK-ind-add-read(10,3)at-overwrite-mem-update-other(11,4)hist-ind(20,6)nowrites-lastPersistedtrue(19,4)persistDependentReads-nextwrite(0,0)rely-unpersisted-subset(13,3)restrict-l-R-same(2,0)restrict-t-empty(2,0)take-first-vol-write-no-unpersisted-writes(40,19)