CHASE: A Static Checker for JML's Assignable Clause

Néstor Cataño; Marieke Huisman

doi:10.1007/3-540-36384-X_6

CHASE: A Static Checker for JML's Assignable Clause

Néstor Cataño, Marieke Huisman

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

27 Citations (Scopus)

Abstract

This paper presents a syntactic method to check so-called assignable clauses of annotated Java programs. Assignable clauses describe which variables may be assigned by a method. Their correctness is crucial for reasoning about class specifications. The method that we propose is incomplete, as it only makes a syntactic check and it does not take aliasing or expression evaluation into account, but it provides efficient means to find the most common errors in assignable clauses. This is demonstrated by applying the method to the specification of an industrial case study.

Original language	English
Title of host publication	Verification, Model Checking, and Abstract Interpretation, 4th International Conference, VMCAI 2003, New York, NY, USA, January 9-11, 2002, Proceedings
Editors	Lenore D. Zuck, Paul C. Attie, Agostino Cortesi, Supratik Mukhopadhyay
Publisher	Springer
Pages	26-40
Number of pages	15
DOIs	https://doi.org/10.1007/3-540-36384-X_6
Publication status	Published - 2003
Externally published	Yes
Event	4th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2003 - New York, United States Duration: 9 Jan 2003 → 11 Jan 2003 Conference number: 4

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	2575

Conference

Conference	4th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2003
Abbreviated title	VMCAI 2003
Country/Territory	United States
City	New York
Period	9/01/03 → 11/01/03

Access to Document

10.1007/3-540-36384-X_6

Cite this

Cataño, N., & Huisman, M. (2003). CHASE: A Static Checker for JML's Assignable Clause. In L. D. Zuck, P. C. Attie, A. Cortesi, & S. Mukhopadhyay (Eds.), Verification, Model Checking, and Abstract Interpretation, 4th International Conference, VMCAI 2003, New York, NY, USA, January 9-11, 2002, Proceedings (pp. 26-40). (Lecture Notes in Computer Science; Vol. 2575). Springer. https://doi.org/10.1007/3-540-36384-X_6

Cataño, Néstor ; Huisman, Marieke. / CHASE: A Static Checker for JML's Assignable Clause. Verification, Model Checking, and Abstract Interpretation, 4th International Conference, VMCAI 2003, New York, NY, USA, January 9-11, 2002, Proceedings. editor / Lenore D. Zuck ; Paul C. Attie ; Agostino Cortesi ; Supratik Mukhopadhyay. Springer, 2003. pp. 26-40 (Lecture Notes in Computer Science).

@inproceedings{2d12fcdb6cf54b658d198112028ee44f,

title = "CHASE: A Static Checker for JML's Assignable Clause",

abstract = "This paper presents a syntactic method to check so-called assignable clauses of annotated Java programs. Assignable clauses describe which variables may be assigned by a method. Their correctness is crucial for reasoning about class specifications. The method that we propose is incomplete, as it only makes a syntactic check and it does not take aliasing or expression evaluation into account, but it provides efficient means to find the most common errors in assignable clauses. This is demonstrated by applying the method to the specification of an industrial case study.",

author = "N{\'e}stor Cata{\~n}o and Marieke Huisman",

year = "2003",

doi = "10.1007/3-540-36384-X_6",

language = "English",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "26--40",

editor = "Zuck, {Lenore D.} and Attie, {Paul C.} and Agostino Cortesi and Supratik Mukhopadhyay",

booktitle = "Verification, Model Checking, and Abstract Interpretation, 4th International Conference, VMCAI 2003, New York, NY, USA, January 9-11, 2002, Proceedings",

address = "Germany",

note = "4th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2003, VMCAI 2003 ; Conference date: 09-01-2003 Through 11-01-2003",

}

Cataño, N & Huisman, M 2003, CHASE: A Static Checker for JML's Assignable Clause. in LD Zuck, PC Attie, A Cortesi & S Mukhopadhyay (eds), Verification, Model Checking, and Abstract Interpretation, 4th International Conference, VMCAI 2003, New York, NY, USA, January 9-11, 2002, Proceedings. Lecture Notes in Computer Science, vol. 2575, Springer, pp. 26-40, 4th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2003, New York, New York, United States, 9/01/03. https://doi.org/10.1007/3-540-36384-X_6

CHASE: A Static Checker for JML's Assignable Clause. / Cataño, Néstor; Huisman, Marieke.
Verification, Model Checking, and Abstract Interpretation, 4th International Conference, VMCAI 2003, New York, NY, USA, January 9-11, 2002, Proceedings. ed. / Lenore D. Zuck; Paul C. Attie; Agostino Cortesi; Supratik Mukhopadhyay. Springer, 2003. p. 26-40 (Lecture Notes in Computer Science; Vol. 2575).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - CHASE: A Static Checker for JML's Assignable Clause

AU - Cataño, Néstor

AU - Huisman, Marieke

N1 - Conference code: 4

PY - 2003

Y1 - 2003

N2 - This paper presents a syntactic method to check so-called assignable clauses of annotated Java programs. Assignable clauses describe which variables may be assigned by a method. Their correctness is crucial for reasoning about class specifications. The method that we propose is incomplete, as it only makes a syntactic check and it does not take aliasing or expression evaluation into account, but it provides efficient means to find the most common errors in assignable clauses. This is demonstrated by applying the method to the specification of an industrial case study.

AB - This paper presents a syntactic method to check so-called assignable clauses of annotated Java programs. Assignable clauses describe which variables may be assigned by a method. Their correctness is crucial for reasoning about class specifications. The method that we propose is incomplete, as it only makes a syntactic check and it does not take aliasing or expression evaluation into account, but it provides efficient means to find the most common errors in assignable clauses. This is demonstrated by applying the method to the specification of an industrial case study.

U2 - 10.1007/3-540-36384-X_6

DO - 10.1007/3-540-36384-X_6

M3 - Conference contribution

T3 - Lecture Notes in Computer Science

SP - 26

EP - 40

BT - Verification, Model Checking, and Abstract Interpretation, 4th International Conference, VMCAI 2003, New York, NY, USA, January 9-11, 2002, Proceedings

A2 - Zuck, Lenore D.

A2 - Attie, Paul C.

A2 - Cortesi, Agostino

A2 - Mukhopadhyay, Supratik

PB - Springer

T2 - 4th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2003

Y2 - 9 January 2003 through 11 January 2003

ER -

Cataño N, Huisman M. CHASE: A Static Checker for JML's Assignable Clause. In Zuck LD, Attie PC, Cortesi A, Mukhopadhyay S, editors, Verification, Model Checking, and Abstract Interpretation, 4th International Conference, VMCAI 2003, New York, NY, USA, January 9-11, 2002, Proceedings. Springer. 2003. p. 26-40. (Lecture Notes in Computer Science). doi: 10.1007/3-540-36384-X_6

CHASE: A Static Checker for JML's Assignable Clause

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this