Title :
Runtime Assertion Checking with the XJML tool
Author :
Ramirez-de-Leon, Edgar D. ; Garcia-Alcocer, Eddy A. ; Torres-Martinez, Napoleon ; Chavez-Bosquez, Oscar A. ; Francisco-Leon, Julian J.
Author_Institution :
Univ. Politec. del Golfo de Mexico, Paraiso, Mexico
Abstract :
Since the conception of the Java Modeling Language (JML), many tools, applications and implementations have been done for its support. In this context, the users or developers who want to use JML seem surrounded by many of these tools, applications and so on. Looking for a common infrastructure and an independent language to provide a bridge between these tools and JML, it was developed an approach to embedded contracts in the eXtensible Markup Language (XML) for Java: XJML. XJML claims to offer you the ability to separate preconditions, posconditions and class invariants using JML and XML, and then execute Runtime Assertion Checking (RAC), Extended Static Checking (ESC) and/or Full Static Program Verification (FSPV). In this work, we present some experiments and results with XJML and Runtime Assertion Checking, using one Java class.
Keywords :
Java; XML; program verification; software tools; specification languages; ESC; Extensible Markup Language; FSPV; JML; Java Modeling Language; Java class; RAC; XJML tool; class invariant separation; embedded contracts; extended static checking; full-static program verification; poscondition separation; precondition separation; runtime assertion checking; Communities; Context; Contracts; Hardware; Java; Runtime; XML;
Conference_Titel :
Biennial Congress of Argentina (ARGENCON), 2014 IEEE
Conference_Location :
Bariloche
Print_ISBN :
978-1-4799-4270-1
DOI :
10.1109/ARGENCON.2014.6868486