Gary T. Leavens, Albert L. Baker, Clyde Ruby · 1998
JML is a behavioral interface specification language tailored to Java. It also allows assertions to be intermixed with Java code, as an aid to verification and debugging. JML is designed to be used by working software engineers, and requires only modest mathematical training. To achieve this goal, JML uses Eiffel-style assertion syntax combined with the model-based approach to specifications typified by VDM and Larch. However, JML supports quantifiers, specification-only variables, frame conditions, and other enhancements that make it more expressive for specification than Eiffel. This paper discusses the goals of JML, the overall approach, and prospects for giving JML a formal semantics through a verification logic. 1 Introduction JML [23], which stands for "Java Modeling Language," is a behavioral interface specification language (BISL) [44] designed to specify Java [2, 9] modules. Java modules are classes and interfaces. A behavioral interface specification describes both ...
Cited by 0
Don Brutzman Code, Don Brutzman · 1998
. The Virtual Reality Modeling Language (VRML) and Java provide a standardized, portable and platformindependent way to render dynamic, interactive 3D scenes across the Internet. Integrating two powerful and portable software languages provides interactive 3D graphics plus complete programming capabilities plus network access. Intended for programmers and scene authors, this paper provides a VRML overview, synopsizes the open development history of the specification, provides a condensed summary of VRML 3D graphics nodes and scene graph topology, describes how Java interacts with VRML through detailed examples, and examines a variety of VRML/Java future developments. Overview. The Web is being extended to three spatial dimensions thanks to VRML, a dynamic 3D scene description language that can include embedded behaviors and camera animation. A rich set of graphics primitives provides a common-denominator file format which can be used to describe a wide variety of 3D scenes and objects...
Cited by 0
Gary T. Leavens, Yoonsik Cheon · 2005
Cited by 0
Marieke Huisman, Wolfgang Ahrendt, Daniel Grahl et al. · Lecture notes in computer science · 2016
Cited by 11Open access
Henrique Rebêlo, Sérgio Soares, Ricardo Lima et al. · 2008
The Java Modeling Language (JML) is a behavioral interface specification language (BISL) designed for Java. It was developed to improve functional software correctness of Java applications. However, instrumented object program generated by the JML compiler use the Java reflection mechanism and data structures not supported by Java ME applications. To deal with this limitation, we propose the use of AspectJ to implement a new JML compiler, which generates an instrumented bytecode compliant with both Java SE and Java ME applications. The paper includes a comparative study to demonstrate the quality of the final code generated by our compiler. The size of the code is compared against the code generated by an existent JML compiler. Moreover, we evaluate the amount of additional code required to implement the JML assertions in Java applications. Results indicate that the overhead in code size produced by our compiler is very small, which is essential for Java ME applications.
Cited by 24
Daniel Bruns · Repository KITopen (Karlsruhe Institute of Technology) · 2009
Diese Arbeit beschäftigt sich mit der Semantik der Java Modeling Language (JML). JML is eine weitverbreitete Spezifikationssprache, die speziell auf Java zugeschnitten ist und sowohl zur statischen als auch zur Laufzeitanalyse von Programmen verwandt wird. Bislang beschränkt sich die offizielle Spezifikation von JML auf eine weitgehend verbale Definition der Semantik, die zudem teilweise unvollständig oder widersprüchlich ist. Daraus erwächst unter anderem, dass die verschiedenen Software-Werkzeuge, die JML implementieren, Sprachelemente der JML unterschiedlich auslegen. Bisherige Arbeiten zur formalen Semantik basieren auf Logiken höherer Ordnung oder dynamischen Logiken. In dieser Arbeit wird ein Ansatz vorgestellt, der nur auf elementaren mathematischen Konzepten wie Mengen, Funktionen und Prädikatenlogik erster Ordnung beruht. In dieser Arbeit wird eine simple Abstraktion einer Maschine vorgestellt, auf der der semantische Unterbau basiert, auf welchen Ausdrücke und Spezifikationen von JML abgebildet werden, um eine nahezu vollständige Übersicht der Spezifikationen für sequentielle Java-Programme zu entwickeln.
Cited by 8Open access
Pfeffermann, Nicole, Rotfuß, Christine · Repository of Futwangen University of Applied Sciences (Furtwangen University) · 2016
Cited by 0
Don Brutzman · Communications of the ACM · 1998
article Free Access Share on The virtual reality modeling language and Java Author: Don Brutzman Naval Postgraduate School, Monterey, CA; and VRML Consortium Naval Postgraduate School, Monterey, CA; and VRML ConsortiumView Profile Authors Info & Claims Communications of the ACMVolume 41Issue 6June 1998pp 57–64https://doi.org/10.1145/276609.276620Published:01 June 1998Publication History 68citation1,446DownloadsMetricsTotal Citations68Total Downloads1,446Last 12 Months163Last 6 weeks24 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF
Cited by 390Open access
Kristina Boysen Taylor · 2008
Design by contract specification languages help programmers write their intentions for a piece of code in a formal mathematical language. Most programming languages do not have built-in syntax for such specifications, so many design by contract languages place specifications in comments. The Java Modeling Language (JML) is one such specification language for Java that uses comments to specify contracts. However, starting with version 5, Java has introduced annotations, a syntactical structure to place metadata in various places in the code. This thesis proposes an initial design to writing JML contracts in the Java 5 annotation syntax and evaluates several criteria in the areas of specification languages and Java language design: whether these annotations are expressive enough to take advantage of annotation simplicity and tool support, and whether the annotation syntax is expressive enough to support handling a large specification language such as JML.
Cited by 4
Danni Yu · 2011
Cited by 0
Souza Neto, Plácido Antônio de · Portuguese National Funding Agency for Science, Research and Technology (RCAAP Project by FCT) · 2014
Métodos formais poderiam ser usados para especificar e verificar software on-card em aplicações Java Card. O estilo de programação para smart cards requer verificação\nem tempo de execução para condições de entrada em todos os métodos Java Card, onde o objetivo principal é preservar os dados do cartão. Projeto por Contrato, em particular, a\nlinguagem JML, é uma opção para este tipo de desenvolvimento e verificação, pelo fato da verificação em tempo de execução ser parte da implementação pela JML. Contudo, JML e suas respectivas ferramentas para verificação em tempo de execução não foram projetadas com o foco nas limitações Java Card, sendo, dessa forma, não compatíveis com Java Card. Nesta dissertação, analisamos o quanto esta situação é realmente intrínseca às limitações Java Card e, se é possível re-definir a JML e suas ferramentas. Propomos\nrequisitos para uma nova linguagem, a qual é compatível com Java Card e apresentamos como o compilador desta linguagem pode ser construído. JCML retira da JML aspectos não definidos em Java Card, como por exemplo, concorrência e tipos não suportados. Isto pode não ser o bastante, contudo, sem o esforço em otimização de código de verificação\ngerado pelo compilador, não é possível gerar código de verificação para rodar no cartão. O compilador JCML, apesar de ser bem mais restrito em relação ao compilador JML,\nestá habilitado a gerar código de verificação compatível com Java Card, para algumas especificações lightweight. Como conclusão, apresentamos uma variante da JML compatível\ncom Java Card, JCML (Java Card Modeling Language), com uma versão de seu compilador
Cited by 0Open access
Daniel Bruns · Informatik-Spektrum · 2011
Cited by 0
Souza Neto, Plácido Antônio de · Americanae (AECID Library) · 2014
Cited by 0Open access
Yoonsik Cheon · 2003
The Java Modeling Language (JML) is a formal behavioral interface specification language (BISL) for Java. JML has many advances including specification-only declarations, specifications of interfaces, stateful interfaces, multiple inheritance of specifications, and behavioral subtyping. An approach to runtime assertion checking of JML assertions is presented and implemented as a JML compiler to translate Java programs annotated with JML specifications into Java bytecode. The compiled bytecode transparently checks JML specifications at runtime. The JML compiler supports separate and modular compilation. The approach brings programming benefits such as debugging and testing to BISLs and also helps programmers to use BISLs in their daily programming.;A set of translation rules are defined from JML expressions into assertion checking code. The translation rules handle various kinds of undefinedness, such as runtime exceptions and non-executable constructs, in such a way as to both satisfy the standard rules of logic and detect as many assertion violations as possible. The rules also support various forms of quantifiers. Specification-only declarations such as model fields, ghost fields, and model methods are translated into access methods; e.g., an access method for a model field is an abstraction function that calculates an abstract value from the program state. The specification state of a stateful interface, due to specification-only fields such as ghost fields, is represented as a separate assertion class. Thus, an object's specification state is distributed over the object itself and one assertion object for each interface that its class implements. Assertion checking is also distributed in that a subtype delegates the responsibility of checking inherited specifications to its supertypes (or the assertion classes of its superinterfaces). The delegation approach supports multiple inheritance, and is modular.;Finally, the effectiveness and practicality of runtime assertion checking is demonstrated by applying it to program testing. An approach is implemented that significantly automates unit testing. The key idea of the approach is to view interface specifications as test oracles and to use the runtime assertion checker as the decision procedure of the test oracles. The approach also shows that the runtime assertion checker can be an effective framework for developing specification-based tools.
Cited by 214Open access
Lederer, Edgar · Institutional Repository (IHS Vienna) · 2008
Cited by 0Open access
Michael Rawding, Bruno Andriamanalimanana, Advisor et al. · SUNY Digital Repository Support (State University of New York System) · 2017
A project presented to the Department of Computer and Information Sciences State University of New York Polytechnic Institute at Utica.
Cited by 0Open access
Wenhui Sun, Yuting Sun, Zhifei Zhang et al. · 2015
Cited by 0
Niethammer, Philipp · Fachbereich Informatik (University of Stuttgart) · 2016
Cited by 0
Yoonsik Cheon, Yoonsik Cheon, Gary T. Leavens et al. · Iowa State University Digital Repository (Iowa State University) · 2002
Debugging is made difficult by the need to precisely describe what each piece of the software is supposed to do, and to write code to defend modules against the errors of other modules; if this is not done it is difficult to assign blame to a small part of the program when things go wrong. Similarly, unit testing also needs precise descriptions of behavior, and is made difficult by the need to write test oracles. However, debugging and testing consume a significant fraction of the cost of software development and maintenance efforts. Inadequate debugging and testing also contribute to quality problems. We describe a runtime assertion checker for the Java Modeling Language (JML) that helps in assigning blame during debugging and in automatic generation of test oracles. It represents a significant advance over the current state of the art, because it can deal with very abstract specifications which hide representation details, and other features such as quantifiers, and inheritance of specifications. Yet JML specifications have a syntax that is easily understood by programmers. Thus, JML's runtime assertion checker has the potential for decreasing the cost of debugging and testing.
Cited by 18Open access
Wilhelm Kärde · 2011
This is a study on the Java Modeling language, presenting its main features and applying them onto an algorithm based upon Binary Decision Diagrams. JML is a Design by Contract tool for java. The principal idea behind Design by Contract is that clients calling methods in a class have a contract with each other. These contracts consist of pre- and post-conditions that are to be validated before and after the execution of any method with such a contract.As interesting as it was studying JML, at the implementation stage it became clear that the JML2 tool set was not upgraded for any java upgrades beyond java 1.4. Using generic types and other language features such as the for-each loop was not recognized by the JML compiler.However, once up and running with a J2SE4 environment, many advantages could be discovered. The runtime assertion checker worked great as a bug prevention tool and the JML specifications serve as a good way to document code properly. More important though is the way it forces the developer to take into consideration all the different relationships between classes and their methods and also to define set invariants to hold for these.
Cited by 0