Open Access. Powered by Scholars. Published by Universities.®
Physical Sciences and Mathematics Commons™
Open Access. Powered by Scholars. Published by Universities.®
Articles 1 - 2 of 2
Full-Text Articles in Physical Sciences and Mathematics
Enhancing The Expressiveness Of The Cleanjava Language, Melisa Vela, Yoonsik Cheon
Enhancing The Expressiveness Of The Cleanjava Language, Melisa Vela, Yoonsik Cheon
Departmental Technical Reports (CS)
The CleanJava language is a formal annotation language for Java to support Cleanroom-style functional program verification that views a program as a mathematical function from one program state to another. The CleanJava notation is based on the Java expression syntax with a few extensions, and thus its vocabulary is somewhat limited to that of Java. This often makes it difficult to specify the rich semantics of a Java program in a succinct and natural way that is easy to manipulate for formal correctness reasoning. In this paper we propose to make the CleanJava language more expressive by supporting user-defined mathematical …
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. …