University of Twente Student Theses
Specification and verification of selected parts of the Java Collections Framework using JML* and KeY
Wal, Jelmer ter (2013) Specification and verification of selected parts of the Java Collections Framework using JML* and KeY.
|
PDF
2MB |
| Abstract: | In this thesis JML* (an extension for JML used by the static verification tool KeY) is used to formalize the behavior of several interfaces and classes, part of the Java Collections Framework. For these specifications several specification styles were used, e.g., making use of model fields, ghost fields, pure methods and abstract data types, which aids in getting an understanding of which style would contribute to better understandability, extensibility and verifiability of JML* specifications. After specifying several interfaces and classes, a large part of the specifications has been verified with KeY. To see whether the specifications made are understandable, a group of people only familiar with basic JML has been asked to fill out a questionnaire. The questionnaire asked whether certain methods – that represent the overall style of specifications done – would be verifiable. Most of the answers provided, suggested that not just the specifications provided, but JML in general is not straightforward to understand, e.g., people have the idea specifications are not verifiable when they do not cover the complete behavior of a method, and additionally the use of model fields as well as invariants is not completely clear. The use of abstract data types (i.e., sequences) as well as framing of methods – specifying the set of locations that might be changed by a method – did not cause a lot of additional confusion for the participants in general. To validate findings about understandability, extensibility and verifiability, a group of experts in the fields of JML* and KeY (i.e., the KeY developers) have been asked to fill out a questionnaire. Depending on one’s experience it might be the case that a specific construct is better for understandability as well as extensibility than the other. All things considered, ghost fields seem to be worse for understandability and extensibility compared to other constructs as they need to update state for every method that affects them. Ghost fields are, however, easier for verifiability though, since – at least for KeY – they can be treated like actual code. Higher forms of abstraction, i.e., using model fields or model methods seem to be more problematic for verification as they can be very complex, and verification tools need to be provided with manual instantiations to reason about them. Moreover, higher abstraction also leads to improved understandability and extensibility. |
| Item Type: | Essay (Master) |
| Faculty: | EEMCS: Electrical Engineering, Mathematics and Computer Science |
| Subject: | 54 computer science |
| Programme: | Computer Science MSc (60300) |
| Link to this item: | https://purl.utwente.nl/essays/64428 |
| Export this item as: | BibTeX EndNote HTML Citation Reference Manager |
Show download statistics for this publication
Show download statistics for this publicationRepository Staff Only: item control page