Differences

This shows you the differences between two versions of the page.

--- verifying_data_structures_using_jahob [2007/06/21 11:53]
kremena.diatchka
+++ verifying_data_structures_using_jahob [2007/06/29 21:06]
kremena.diatchka
@@ Line 5: / Line 5: @@
 Our goal is to verify the implementations in Java of simple data structures using Jahob.
-==== Verified ====
+==== Abstract ====
+We have implemented some simple data structures in Java, provided specifications for properties they must specify, and attempted to verify that the implementation is correct with respect to these specifications using the verification tool Jahob. We have fully verified the implementations of a singly-linked list with a header node and a queue. All methods of a singly-linked cyclic list, doubly-linked cyclic list and leaf-linked tree also verify, but these classes require further work to ensure the specifications are correct in the initial state of the class. This report presents a brief overview of data structure verification using Jahob, and then continues with a detailed explanation of the specifications we provided. We conclude by summarizing our contributions, commenting on what we have learned, and suggesting directions for future work.
-  * Linked list with header node
+Final report:
-  * Queue (partial specification)
+{{feride-kremena_report.pdf| Data Structure Verification Using Jahob}}
-  * Cyclic list (probable bug with verification of initial state)
+Code:
-==== In progress ====
+{{feride_kremena_code.tar.gz| Data structures verified with Jahob }}
-  * Leaf-linked tree
-Implementation done, some class invariants written. TO DO: focus on expanding specifications: procedure contracts and loop invariants.
-  * Doubly-linked cyclic list
-Init() and add() methods verify, problem with loop invariant for member method.