– Null pointer exceptions – Better detecting them statically using JML …
JML Reference Manual DRAFT, $Revision: 1.220 $ $Date: 2008/01/08 22:43:42 $ (2008)
Gary T. Leavens, Erik Poll, Curtis Clifton, Yoonsik Cheon, Clyde Ruby, David Cok, ...
Permission is granted for you to make copies of this manual for educational and scholarly purposes, and for commercial use in specifying software, but the copies may not be sold or otherwise used for...
with contributions from (2008)
Joseph R. Kiniry, Patrice Chalin, Clément Hurlin, Cees-bart Breunesse, Julien Charles, ...
Automatic verification by means of extended static checking (ESC) has seen some success in industry and academia due to its lightweight and easy-to-use nature. Unfortunately, ESC comes at a cost: a...
John Boyland, Alex Buckley, Patrice Chalin, Dave Clarke, Paola Giannini, Marieke Huisman, ...
This report contains the papers presented at FTfJP ’07: 9th workshop on Formal
1.1 Use Case Definition (2008)
Daniel Sinnig, Frédéric Rioux, Patrice Chalin
This paper highlights the preliminary results of a survey that is currently being conducted to identify if and how use cases are employed by professionals and researchers. In addition, this paper...
Consistency between Task Models and Use Cases (2008)
Daniel Sinnig, Patrice Chalin, Ferhat Khendek
Abstract. Use cases are the notation of choice for functional requirements documentation, whereas task models are used as a starting point for user interface design. In this paper, we motivate the...
John Boyland, Alex Buckley, Patrice Chalin, Dave Clarke, Paola Giannini, Marieke Huisman, ...
This report contains the papers presented at FTfJP ’07: 9th workshop on Formal
Common Semantics for Use Cases and Task Models (2008)
Daniel Sinnig, Patrice Chalin, Ferhat Khendek
In this paper, we introduce a common semantic framework for developing and formally modeling use cases and task models. Use cases are the notation of choice for functional requirements specification...
Effective and Efficient Runtime Assertion Checking for JML Through Strong Validity (2008)
Frederic Rioux, Patrice Chalin
www.dsrg.org Abstract. Previously, we presented an assertion semantics for JML based on “strong validity ” in which an assertion is taken to be valid precisely when it is defined and true....
with contributions from (2008)
Joseph R. Kiniry, Patrice Chalin, Clément Hurlin, Cees-bart Breunesse, David Cok, ...
Automatic verification by means of extended static checking (ESC) has seen some success in industry and academia due to its lightweight and easy-to-use nature. Unfortunately, ESC comes at a cost: a...
Shortcomings of LCL 2.4 (2007)
Patrice Chalin, Patrice Chalin
Critical assessment of the strengths and weaknesses of a language are essential for its evolution. In this paper we present some of the more significant shortcomings of LCL 2.4, a Larch/C...
Patrice Chalin, Perry R. James, George Karabotsos, Patrice Chalin, Perry R. James, George Karabotsos
languages; F.3.1 [Logics and Meanings of Programs] Specifying and Verifying and Reasoning
G.: An integrated verification environment for JML: Architecture and early results (2007)
Patrice Chalin, Perry R. James, George Karabotsos
Tool support for the Java Modeling Language (JML) is a very pressing problem. A main issue with current tools is their architecture: the cost of keeping up with the evolution of Java is prohibitively...
Patrice Chalin, Patrice Chalin
of Programs] Specifying and Verifying and Reasoning about Programs.
Beyond assertions: Advanced specification and verification with JML and ESC/Java2 (2006)
Erik Poll, Patrice Chalin, David Cok, Joe Kiniry, Gary T. Leavens
Abstract. Many state-based specification languages, including the Java Modeling Language (JML), contain at their core specification constructs familiar to most computer science and software...
Towards Support for Non-null Types and Non-null-by-default in Java (2006)
Abstract. This paper begins with a survey of current programming language support for non-null types and annotations, with a particular focus on extensions to Java. With the advent of Java 5...
Beyond assertions: Advanced specification and verification with JML and ESC/Java2 (2006)
Patrice Chalin, Joseph R. Kiniry, Gary T. Leavens, Erik Poll
Abstract. Many state-based specification languages, including the Java Modeling Language (JML), contain at their core specification constructs familiar to most undergraduates: e.g., assertions, pre-...
Early detection of JML specification errors using ESC/Java2 (2006)
The earlier errors are found, the less costly they are to fix. This also holds true of errors in specifications. While research into Static Program Verification (SPV) in general, and Extended Static...
Beyond assertions: Advanced specification and verification with JML and ESC/Java2 (2006)
Patrice Chalin, Joseph R. Kiniry, Gary T. Leavens, Erik Poll
Abstract. Many state-based specification languages, including the Java Modeling Language (JML), contain at their core specification constructs familiar to most undergraduates: e.g., assertions, pre-...
of Programs] Specifying and Verifying and Reasoning about Programs.
Non-null References by Default in the Java Modeling Language (2005)
Patrice Chalin, Frédéric Rioux
Based on our experiences and those of our peers, we hypothesized that in Java code, the majority of declarations that are of reference types are meant to be non-null. Unfortunately, the Java Modeling...
Patrice Chalin, Frédéric Rioux
� Section 2.2.2: of course the assertions can be atomic predicates of the given forms.
of Programs] Specifying and Verifying and Reasoning about Programs.
Reassessing JML's Logical Foundation (2005)
www.cs.concordia.ca/~chalin Abstract. Early in the design of the Java Modeling Language (JML) care was taken in the choice of its logical foundation to ensure that JML could accommodate run-time...
Leavens JML Framed! 3 Behavioral Interface Specification (2004)
Gary T. Leavens, Yoonsik Cheon, Curtis Clifton, Rustan Leino, Bart Jacobs, Erik Poll, ...
Behavioral interface specification language, tailored to Java • Records detailed designs • Pre- and postconditions, invariants,... • Synthesizes ideas in sequential specification
2 Design by Contract and Behavioral Interface Specification.................................................................... 2
JML support for primitive arbitrary precision numeric types: definition and semantics (2003)
www.cs.concordia.ca/~faculty/chalin The Java Modeling Language, JML, is a notation for specifying and describing the detailed design and
Patrice Chalin, Peter Grogono, T. Radhakrishnan
Abstract. We present some of the more significant shortcomings of LCL, a Larch/C specification language used to document the interfaces of modules written in ISO C. We illustrate inadequacies in the...
Copying, sharing, and aliasing (1994)
Study of the history of programming languages reveals a subtle interplay between semantics and implementation. Early languages, designed for maximum efficiency, provided simple abstractions of the...
Copying, sharing, and aliasing (1994)
Study of the history of programming languages reveals a subtle interplay between semantics and implementation. Early languages, designed for maximum efficiency, provided simple abstractions of the...
A case study of the formal development of an object manager / (1989)
Thesis (M.Comp.Sc.)--Concordia University, Dept. of Computer Science, 1989.
and Hanne Riis Nielson. 2-level -lifting (1988)
Joseph R. Kiniry, Alan E. Morkan, Dermot Cochran, Fintan Fairmichael, Patrice Chalin, Martijn Oostdijk, ...
Abstract. Remote internet voting incorporates many of the core challenges of trusted global computing. In this paper, we present the Kiezen op Afstand 4 (KOA) system. KOA is a Free Software, remote...