An overview of JML tools and applications

The Java Modeling Language (JML) can be used to specify the detailed design of Java classes and interfaces by adding annotations to Java source files. The aim of JML is to provide a specification language that is easy to use for Java programmers and that is supported by a wide range of tools for specification typechecking, runtime debugging, static analysis, and verification.This paper gives an overview of the main ideas behind JML, details about JML’s wide range of tools, and a glimpse into existing applications of JML.     

Hand use and gestural communication in chimpanzees (Pan troglodytes).

Hand use in gestural communication was examined in 115 captive chimpanzees (Pan troglodytes). Hand use was measured in subjects while they gestured to food placed out of their reach. The distribution of hand use was examined in relation to sex, age, rearing history, gesture type, and whether the subjects vocalized while gesturing. Overall, significantly more chimpanzees, especially females and adults, gestured with their right than with their left hand. Foods begs were more lateralized to the right hand than pointing, and a greater prevalence of right-hand gesturing was found in subjects who simultaneously vocalized than those who did not. Taken together, these data suggest that referential, intentional communicative behaviors, in the form of gestures, are lateralized to the left hemisphere in chimpanzees. (PsycINFO Database Record (c) 2010 APA, all rights reserved)     

Polymorphic type-checking in scheme

This paper presents a type-inference system for Scheme that is designed to be used by students in an introductory programming course. The major goal of the work is to present a type system that is simple enough to be used by beginner students, yet is powerful enough to express the ideas of polymorphism, abstract data types (ADTs), and higher-order procedures. The system also performs some rudimentary syntax checking. The system uses subtyping, but only in a primitive fashion. It has a type datum which is a supertype of all types, and a type poof which is a subtype of all types. It uses intersection types to control the use of datum and to generate simple but accurate types.     

Multiple-plane-wave theory of gap anisotropy in Al

The variation over the Fermi surface of the superconducting gap edge ₀ (k) has been calculated for Al. We include in the computations a realistic Fermi surface, multiple-plane-wave electron-phonon matrix elements, and realistic phonons. The computations proceed from directional electron-phonon spectral weights which contain the information on the phonon-mediated electron-electron interaction for a given electron ¦k. To relate the microscopic parameters to the gaps, we use the equations due to Leavens and Carbotte. They are an approximate version of the Eliashberg equations valid for the gap edge in the weak coupling limit. The results are used to compute the pure single-crystal transition temperature.Research supported in part by the National Research Council of Canada.     

Automated translation of VDM to JML-annotated Java

International Journal on Software Tools for Technology Transfer - When a system specified using the Vienna Development Method (VDM) is realised using code-generation, no guarantees are currently...     

The whole-hand point: The structure and function of pointing from a comparative perspective.

Pointing by monkeys, apes, and human infants is reviewed and compared. Pointing with the index finger is a species-typical human gesture, although human infants exhibit more whole-hand pointing than is commonly appreciated. Captive monkeys and feral apes have been reported to only rarely "spontaneously" point, although apes in captivity frequently acquire pointing, both with the index finger and with the whole hand, without explicit training. Captive apes exhibit relatively more gaze alternation while pointing than do human infants about 1 year old. Human infants are relatively more vocal while pointing than are captive apes, consistent with paralinguistic use of pointing. (PsycINFO Database Record (c) 2010 APA, all rights reserved)     

Protective Interface Specifications

The interface specification of a procedure describes the procedure's behaviour using pre- and postconditions. These pre- and postconditions are written using various functions. If some of these functions are partial, or underspecified, then the procedure specification may not be well-defined. We show how to write pre- and postcondition specifications that avoid such problems, by having the precondition “protect” the postcondition from the effects of partiality and underspecification. We formalize the notion of protection from partiality in the context of specification languages like VDM-SL and COLD-K. We also formalize the notion of protection from underspecification for the Larch family of specification languages, and for Larch show how one can prove that a procedure specification is protected from the effects of underspecification. Received October 1997 / Accepted in revised form March 1998     

Model variables: cleanly supporting abstraction in design by contract

In design by contract (DBC), assertions are typically written using program variables and query methods. The lack of separation between program code and assertions is confusing, because readers do not know what code is intended for use in the program and what code is only intended for specification purposes. This lack of separation also creates a potential runtime performance penalty, even when runtime assertion checks are disabled, due to both the increased memory footprint of the program and the execution of code maintaining that part of the program's state intended for use in specifications. To solve these problems, we present a new way of writing and checking DBC assertions without directly referring to concrete program states, using ‘model’, i.e. specification‐only, variables and methods. The use of model variables and methods does not incur the problems mentioned above, but it also allow one to write more easily assertions that are abstract, concise, and independent of representation details, and hence more readable and maintainable. We implemented these features in the runtime assertion checker for the Java Modeling Language (JML), but the approach could also be implemented in other DBC tools. Copyright © 2005 John Wiley & Sons, Ltd.     

Specification and verification challenges for sequential object-oriented programs

The state of knowledge in how to specify sequential programs in object-oriented languages such as Java and C# and the state of the art in automated verification tools for such programs have made measurable progress in the last several years. This paper describes several remaining challenges and approaches to their solution.     

Modular specification and verification of object-oriented programs

A method for modular specification and verification using the ideas of subtype and normal type is presented. The method corresponds to informal techniques used by object-oriented programmers. The key idea is that objects of a subtype must behave like objects of that type's supertypes. An example program is used to show the reasoning problems that supertype abstraction may cause and how the method resolves them. Subtype polymorphism is addressed, and specification and verification update is discussed. A set of syntactic and semantic constraints on subtype relationships, which formalize the intuition that each object of a subtype must behave like some object of each of its supertypes, is examined. These constraints are the key to the soundness of the method. To state them precisely, a formal model of abstract type specifications is used