A Universe-Type-Based Verification Technique for Mutable Static Fields and Methods (Work in Progress)
File(s)
Accepted version
Author(s)
Summers, A
Drossopoulou, S
Müller, P
Type
Conference Paper
Abstract
We present a novel technique for the verification of invariants\r\nin the setting of a Java-like language including static fields and methods. The technique is a generalisation of the existing \r\nVisibility Technique of Mueller et al., which employs universe types.\r\n\r\nIn order to cater for mutable static fields, we extend this topology to\r\nmultiple trees (a forest), where each tree is rooted in a class. This allows classes to naturally own object instances as their static fields.We describe how to extend the Visibility Technique to this topology, incorporating extra flexibility for the treatment of static methods.\r\nWe encounter a potential source of callbacks not present in the original\r\ntechnique, and show how to overcome this using an effects system. To\r\nallow flexible and modular verification, we refine our topology with a\r\nhierarchy of `levels'
Date Issued
2008-07
Citation
2008, pp.111-124
Source Title
10th Workshop on Formal techniques for Java-like Programming (FTfJP 2008)
Start Page
111
End Page
124
Copyright Statement
© 2008 The Authors
Identifier
http://www-sop.inria.fr/everest/events/FTfJP08/
Source
10th Workshop on Formal techniques for Java-like Programming (FTfJP 2008)
Source Place
Paphos, Cyprus
Start Date
2008-07-08
Finish Date
2008-07-08
Coverage Spatial
Paphos, Cyprus