RSRG: Benchmarks: Sorting
Entries of a Queue Data Abstraction
2008 May 23
Please note that all files can be opened with a simple word processor, regardless of the extensions.
- Concept (specification): Queue_Template
- Enhancement (specification):
Sorting_Capability version 1
- Realization (implementation): Erroneous Sorting_Realiz_v1
for Sorting_Capability of Queue_Template
- Verification Conditions: Easy-to-read Format
- Verification
Conditions: Isabelle Format (subsumed by the ones below; not shown)
- Results: Isabelle
finds errors in attempting to prove the VCs.
- Enhancement (specification):
Sorting_Capability version 1 (version 2 is identical to version 1)
- Realization (implementation): Unprovable Sorting_Realiz_v2
for Sorting_Capability of Queue_Template
- Verification Conditions: Easy-to-read Format
- Verification Conditions: Isabelle Format
- Corresponding
Isabelle String theory
- Results: Isabelle is
unable to prove some of the VCs without human assistance.
- Enhancement (specification):
Sorting_Capability version 3
- Improved and Generalized
Enhancement (specification): Sorting_Capability version forthcoming
Last modified: Wed May 23 10:07:49 EDT
2008