Open Access. Powered by Scholars. Published by Universities.®
Physical Sciences and Mathematics Commons™
Open Access. Powered by Scholars. Published by Universities.®
- Discipline
Articles 1 - 2 of 2
Full-Text Articles in Physical Sciences and Mathematics
Cjc: An Extensible Checker For The Cleanjava Annotation Language, Cesar Yeep
Cjc: An Extensible Checker For The Cleanjava Annotation Language, Cesar Yeep
Departmental Technical Reports (CS)
CleanJava is a formal annotation language for the Java programming language to support a Cleanroom-style functional program verification technique that views programs as mathematical functions. It needs a suite of support tools including a checker that can parse annotations and check them for syntactic and static semantic correctness. The two key requirements of the checker are flexibility and extensibility. Since the language is still under development and refinement, it should be flexible to facilitate language experimentation and accommodate language changes. It should be also extensible to provide base code for developing more advanced support tools like an automated theorem prover. …
Constructing Verifiably Correct Java Programs Using Ocl And Cleanjava, Yoonsik Cheon, Carmen Avila
Constructing Verifiably Correct Java Programs Using Ocl And Cleanjava, Yoonsik Cheon, Carmen Avila
Departmental Technical Reports (CS)
A recent trend in software development is building a precise model that can be used as a basis for the software development. Such a model may enable an automatic generation of working code, and more importantly it provides a foundation for correctness reasoning of code. In this paper we propose a practical approach for constructing a verifiably correct program from such a model. The key idea of our approach is (a) to systematically translate formally-specified design constraints such as class invariants and operation pre and postconditions to code-level annotations and (b) to use the annotations for the correctness proof of …