Automated program repair (APR) tools generally use a test suite to localize bugs and validate patches. These patches may pass the test suite but still be incorrect, which is called overfitting. To better understand the relationship between code coverage and overfitting, we aim to quantify the reduction in overfitting achieved by having more tests to cover branches multiple times, once 100% branch coverage is reached. We also investigate whether having more such tests increases the chances that the generated patch is exact, meaning that the patched program is syntactically the same as the original, high quality correct code in our dataset. Our experiments used three different test suites, each covering all branches in the code: test suites that cover each branch at least 1, 3, or 5 times. We used seven well-known APR tools for Java on a dataset of buggy programs equipped with formal specifications. Using formal methods allows us to reliably and objectively check for overfitting. Our experimental results indicate that enlarging the test suite beyond 100% coverage of branches reduces overfitting. However, beyond a certain threshold, expanding the test suite to cover branches repeatedly does not reduce overfitting.

Testing to detect semantic bugs is essential, especially for critical systems. Coverage-guided fuzzing (CGF) and runtime assertion checking (RAC) are two well-known approaches for detecting semantic bugs. CGF aims to generate test inputs with high code coverage. However, while CGF tools can be equipped with sanitizers to detect a fixed set of semantic bugs, they can otherwise only detect bugs that lead to a crash. Thus, the first problem we address is how to help fuzzers detect previously unknown semantic bugs that do not lead to a crash. Moreover, a CGF tool may not necessarily cover all branches with valid inputs, although invalid inputs are useless for detecting semantic bugs. So, the second problem is how to guide a fuzzer to maximize coverage using only valid inputs. However, RAC monitors the expected behavior of a program dynamically and can only detect a semantic bug when a valid test input shows that the program does not satisfy its specification. Thus, the third problem is how to provide high-quality test inputs for a RAC that can trigger potential bugs. The combination of a CGF tool and RAC solves these problems and can cover branches with valid inputs and detect semantic bugs effectively. Our study uses RAC to guarantee that only valid inputs reach the program under test using the program’s specified preconditions, and it also uses RAC to detect semantic bugs using specified postconditions. A prototype tool was developed for this study, named JMLKelinci+. Our results show that combining a CGF tool with RAC will lead to executing the program under test only with valid inputs and that this technique can effectively detect semantic bugs. Also, this idea improves the feedback given to a CGF tool, enabling it to cover all branches faster in programs with non-trivial preconditions. 1

Formal methods are used for verifying software correctness and reliability, especially for safety- and security-critical systems. After changing or refactoring code, it is often necessary to repair a program’s correctness proof, which can be time-consuming. We describe the problem of automated reasoning repair, provide a public dataset, and suggest some solution directions.

Automated program repair (APR) techniques have shown a promising ability to generate patches that fix program bugs automatically. Typically such APR tools are dynamic in the sense that they find bugs by testing and they validate patches by running a program's test suite. Patches can also be validated manually. However, neither of these methods for validating patches can truly tell whether a patch is correct. Test suites are usually incomplete, and thus APR-generated patches may pass the tests but not be truly correct; in other words, the APR tools may be overfitting to the tests. The possibility of test overfitting leads to manual validation, which is costly, potentially biased, and can also be incomplete. Therefore, we must move past these methods to truly assess APR's overfitting problem.We aim to evaluate the test overfitting problem in dynamic APR tools using ground truth given by a set of programs equipped with formal behavioral specifications. Using these formal specifications and an automated verification tool, we found that there is definitely overfitting in the generated patches of seven well-studied APR tools, although many (about 59%) of the generated patches were indeed correct. Our study further points out two new problems that can affect APR tools: changes to the complexity of programs and numeric problems. An additional contribution is that we introduce the first publicly available data set of formally specified and verified Java programs, their test suites, and buggy variants, each of which has exactly one bug.

Dynamic automated program repair (APR) techniques, which use test suites for bug localization and evaluating candidate patches, have promising results. However, many studies show that machine-generated patches with dynamic APR tools are not always reliable. Recent studies show that enhancing test suites by adding tests will help dynamic APR tools generate more reliable patches. We evaluate the effectiveness of minimally enhancing test suites by adding counterexamples for repaired programs that suffer from test overfitting. We use formal methods as an independent standard for evaluating patches' correctness and for generating counterexamples. Techniques for evaluating patch correctness (both with human reviewers and formal methods) can create false negatives, meaning that the repaired program is correct but is deemed incorrect. A counterexample is a good way to check on reviewer decisions about correctness. Our study evaluated 256 repaired but not verified programs (from the buggy Java+JML dataset); the repairs were generated by seven state-of-the-art dynamic APR tools. Our results show that the counterexample generated by the OpenJML tool could correctly classify all these programs into the categories of “test overfitting” and “false negatives.” After adding tests based on the counterexamples to the test suites, we ran the APR tools on the original buggy programs again and found that: (1) the APR tools were able to generate about 27.3% more correct patches with the enhanced test suite, and (2) the enhanced test suite resulted in the APR tools generating about 83.6% fewer overfitted patches.

Abstract Framing is important for specification and verification, especially in programs that mutate data structures with shared data, such as DAGs. Both separation logic and region logic are successful approaches to framing, with separation logic providing a concise way to reason about data structures that are disjoint, and region logic providing the ability to reason about framing for shared mutable data. In order to obtain the benefits of both logics for programs with shared mutable data, this paper unifies them into a single logic, which can encode both of them and allows them to interoperate. The new logic thus provides a way to reason about program modules specified in a mix of styles.

Specification languages have long featured ways to describe what does not change when an imperative procedure is executed: the so-called frame problem. Solutions to the frame problem are needed for formal verification in imperative programming, as otherwise a verification would not be able to accumulate information from one statement to the next. Region logic is one of the approaches to solving the frame problem. We present a modified version of region logic with fine granularity and introduce conditional effects that allows one to specify more precise frame conditions.

Despite their proven benefits, useful, comprehensible, and efficiently checkable specifications are not widely available. This is primarily because writing useful, non-trivial specifications from scratch is too hard, time consuming, and requires expertise that is not broadly available. Furthermore, the lack of specifications for widely-used libraries and frameworks, caused by the high cost of writing specifications, tends to have a snowball effect. Core libraries lack specifications, which makes specifying applications that use them expensive. To contain the skyrocketing development and maintenance costs of high assurance systems, this self-perpetuating cycle must be broken. The labor cost of specifying programs can be significantly decreased via advances in specification inference and synthesis, and this has been attempted several times, but with limited success. We believe that practical specification inference and synthesis is an idea whose time has come. Fundamental breakthroughs in this area can be achieved by leveraging the collective intelligence available in software artifacts from millions of open source projects. Fine-grained access to such data sets has been unprecedented, but is now easily available. We identify research directions and report our preliminary results on advances in specification inference that can be had by using such data sets to infer specifications.

Verification of a dynamically dispatched method call, E . m (), seems to depend on E ’s dynamic type. To avoid case analysis and allow incremental development, object-oriented program verification uses supertype abstraction. In other words, one reasons about E . m () using m ’s specification for E ’s static type. Supertype abstraction is valid when each subtype in the program is a behavioral subtype. This article semantically formalizes supertype abstraction and behavioral subtyping for a Java-like sequential language with mutation and proves that behavioral subtyping is both necessary and sufficient for the validity of supertype abstraction. Specification inheritance, as in JML, is also formalized and proved to entail behavioral subtyping.

SUMMARY Real‐time and safety‐critical code could benefit from the use of design patterns and frameworks that rely on subtyping and dynamic dispatch. However, modular reasoning about programs that use subtypes requires that each overriding method obeys the specifications of all methods that it overrides. For example, if method scale is specified in a supertype Vector2d to take at most 42 ns to execute, then an override of scale cannot take more than 42 ns to execute in any subtype, such as Vector3d. The problem is that subtype objects typically contain more information, such as the z coordinate in Vector3d, and thus their methods often require more time to execute than the methods they override. In this paper, we show how to specify timing constraints for subtypes in a way that both allows overriding subtype methods to have more time to execute and yet permits precise modular verification and checking of timing constraints. Our techniques allow object‐oriented coding and design patterns based on subtype polymorphism to be used in real‐time and safety‐critical software. Copyright © 2012 John Wiley & Sons, Ltd.

Code comments are important artifacts in software. Javadoc comments are widely used in Java for API specifications. API developers write Javadoc comments, and API users read these comments to understand the API, e.g., reading a Javadoc comment for a method instead of reading the method body. An inconsistency between the Javadoc comment and body for a method indicates either a fault in the body or, effectively, a fault in the comment that can mislead the method callers to introduce faults in their code. We present a novel approach, called @TCOMMENT, for testing Javadoc comments, specifically method properties about null values and related exceptions. Our approach consists of two components. The first component takes as input source files for a Java project and automatically analyzes the English text in Javadoc comments to infer a set of likely properties for a method in the files. The second component generates random tests for these methods, checks the inferred properties, and reports inconsistencies. We evaluated @TCOMMENT on seven open-source projects and found 29 inconsistencies between Javadoc comments and method bodies. We reported 16 of these inconsistencies, and 5 have already been confirmed and fixed by the developers.

Design by Contract (DbC) is a technique for developing and improving functional software correctness through definition of "contracts" between client classes and their suppliers. Such contracts are enforced during runtime and if any of them is violated a runtime error should occur. Runtime assertions checkers (RACs) are a well-known technique that enforces such contracts. Although they are largely used to implement the DbC technique in contemporary languages, like Java, studies have shown that characteristics of contemporary exception handling mechanisms can discard contract violations detected by RACs. As a result, a contract violation may not be reflected in a runtime error, breaking the supporting hypothesis of DbC. This paper presents an error recovery technique for RACs that tackles such limitations. This technique relies on aspect-oriented programming in order to extend the functionalities of existing RACs stopping contract violations from being discarded. We applied the recovery technique on top of five Java-based contemporary RACs (i.e., JML/jml, JML/ajml, JContractor, CEAP, and Jose). Preliminary results have shown that the proposed technique could actually prevent the contract violations from being discarded regardless of the characteristics of the exception handling code of the target application.

Most mainstream specification languages primarily deal with a program's functional behavior. However, for many common problems, besides the system's functionality, it is necessary to be able to express its temporal properties, such as the necessity of calling methods in a certain order. We have developed temporaljmlc, a tool that performs runtime assertion checking of temporal properties specified in an extension of the Java Modeling Language (JML). The benefit of temporaljmlc is that it allows succinct specification of temporal properties that would otherwise be tedious and difficult to specify.

Information hiding controls which parts of a class are visible to non-privileged and privileged clients (e.g., subclasses). This affects detailed design specifications in two ways. First, specifications should not expose hidden class members. As noted in previous work, this is important because such hidden members are not meaningful to all clients. But it also allows changes to hidden implementation details without invalidating correctness proofs for client code, which is important for maintaining verified programs. Second, to enable sound modular reasoning, certain specifications must be visible to clients. We present rules for information hiding in specifications for Java-like languages, and demonstrate their application to the specification language JML. These rules restrict proof obligations to only mention visible class members, but retain soundness. This allows maintenance of implementations and their specifications without affecting client reasoning.

The Java Modeling Language (JML) is widely used in academic research as a common language for formal methods tools that work with Java. JML is a design by contract language that can be used to specify detailed designs of Java programs, frameworks, and class libraries. Over twenty research groups worldwide have built several tools for checking code and finding bugs (see jmlspecs.org).

What we call a''higher-order method" (HOM) is a method that makes mandatory calls to other dynamically-dispatched methods. Examples include template methods as in the Template method design pattern and notify methods in the Observer pattern. HOMs are particularly difficult to reason about, because standard pre- and postcondition specifications cannot describe the mandatory calls. For reasoning about such methods, existing approaches use either higher order logic or traces, but both are complex and verbose.

SAVCBS is a workshop for research and experience reports on the specification and verification of component-based systems.

Abstract 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.

This roadmap describes ways that researchers in four areas---specification languages, program generation, correctness by construction, and programming languages---might help further the goal of verified software. It also describes what advances the "verified software" grand challenge might anticipate or demand from work in these areas. That is, the roadmap is intended to help foster collaboration between the grand challenge and these research areas.A common goal for research in these areas is to establish language designs and tool architectures that would allow multiple annotations and tools to be used on a single program. In the long term, researchers could try to unify these annotations and integrate such tools.

Classical specification and verification techniques support invariants for individual objects whose fields are primitive values, but do not allow sound modular reasoning about invariants involving more complex object structures. Such non-trivial object structures are common, and occur in lists, hash tables, and whenever systems are built in layers. A sound and modular verification technique for layered object structures has to deal with the well-known problem of representation exposure and the problem that invariants of higher layers are potentially violated by methods in lower layers; such methods cannot be modularly shown to preserve these invariants. We generalize classical techniques to cover layered object structures using a refined semantics for invariants based on an ownership model for alias control. This semantics enables sound and modular reasoning. We further extend this ownership technique to even more expressive invariants that gain their modularity by imposing certain visibility requirements.

MultiJava is a conservative extension of the Java programming language that adds symmetric multiple dispatch and open classes. Among other benefits, multiple dispatch provides a solution to the binary method problem. Open classes provide a solution to the extensibility problem of object-oriented programming languages, allowing the modular addition of both new types and new operations to an existing type hierarchy. This article illustrates and motivates the design of MultiJava and describes its modular static typechecking and modular compilation strategies. Although MultiJava extends Java, the key ideas of the language design are applicable to other object-oriented languages, such as C# and C++, and even, with some modifications, to functional languages such as ML.This article also discusses the variety of application domains in which MultiJava has been successfully used by others, including pervasive computing, graphical user interfaces, and compilers. MultiJava allows users to express desired programming idioms in a way that is declarative and supports static typechecking, in contrast to the tedious and type-unsafe workarounds required in Java. MultiJava also provides opportunities for new kinds of extensibility that are not easily available in Java.

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.

This talk will try to frame JML in two senses. The first is the sense of placing JML in the context of other specification languages and tools. This context will be provided by giving a brief introduction to JML, with small examples. The different tools that work with JML also help provide context for the language design in a different way. Another aspect of this context is provided by comparing JML with other design by contract languages, such as Eiffel.The second sense of framing in JML is the more technical one of frame axioms, also known as "modifies clauses". Such frame axioms are critical for reasoning, and are difficult to check at runtime; hence static analysis is a crucial need. We will discuss the semantics of JML's frame axioms, including datagroups, both in a naive sense and with the experimental Universe type system. Both problems in the semantics and checking, as well as some recent work will be presented. Note that some of the recent work on frame axioms in JML, especially extensions with the Universe type system, is joint work with Peter Müller (of ETH Zürich) and Arnd Poetzsch-Heffter of (U. Kaiserslautern). At Iowa State, the development of JML was partially funded by the (US) National Science Foundation under grants CCR-9503168, CCR-9803843, CCR-0097907, and CCR-0113181.

Abstract We present a modular specification technique for frame properties. The technique uses modifies clauses and abstract fields with declared dependencies. Modularity is guaranteed by a programming model that enforces data abstraction by preventing representation and argument exposure, a semantics of modifies clauses that uses a notion of ‘relevant location’, and by modularity rules for dependencies. For concreteness, we adapt this technique to the Java Modeling Language, JML. Copyright © 2003 John Wiley & Sons, Ltd.

Formal techniques for Java programsFormal techniques can help analyze programs, precisely describe program behavior, and verify program properties.Applying such techniques to object-oriented technology is especially interesting because• the object-oriented (OO) paradigm forms the basis for the software component industry with their need for certification techniques, • it is widely used for distributed and network programming and • the potential for reuse in OO programming carries over to reusing specifications and proofs.Such formal techniques are sound, only if based on a formalization of the language itself.Java is a good platform to bridge the gap between formal techniques and practical program development.It plays an important role in these areas and is on the way to becoming a de facto standard because of its reasonably clear semantics and its standardized library.However, Java contains novel language features, which are not yet fully understood.More importantly, Java supports a novel paradigm for program deployment, and improves interactivity, portability and manageability.This paradigm opens new possibilities for abuse and causes concern about security.The ECOOP 2000 workshop on Formal Techniques for Java Programs was held in Sophia Antipolis, France.It was a follow-up for last year's ECOOP workshop on the same topic [1] and the Formal Underpinnings of the Java Paradigm workshop held at OOPSLA '98 [2].Proceedings containing all the papers are available as a technical report of the Computer Science Department of the FernUniversität Hagen [3].This special issue contains extended and refereed versions of four papers, selected from the best papers presented at the workshop.Eva Rose and Kristoffer Rose suggest in their paper 'Java access protection through typing' the integration of a dedicated read-only field access into the Java type system.The advantage is that

We present MultiJava, a backward-compatible extension to Java supporting open classes and symmetric multiple dispatch. Open classes allow one to add to the set of methods that an existing class supports without creating distinct subclasses or editing existing code. Unlike the "Visitor" design pattern, open classes do not require advance planning, and open classes preserve the ability to add new subclasses modularly and safely. Multiple dispatch offers several well-known advantages over the single dispatching of conventional object-oriented languages, including a simple solution to some kinds of "binary method" problems. MultiJava's multiple dispatch retains Java's existing class-based encapsulation properties. We adapt previous theoretical work to allow compilation units to be statically typechecked modularly and safely, ruling out any link-time or run-time type errors. We also present a n compilation scheme that operates modularly and incurs performance overhead only where open classes or multiple dispatching are actually used.

A major problem for object-oriented frameworks and class libraries is how to provide enough information about a superclass, so programmers can safely create new subclasses without giving away the superclass's code. Code inherited from the superclass can call down to methods of the subclass, which may cause nontermination or unexpected behavior. We describe a reasoning technique that allows programmers, who have no access to the code of the superclass, to determine both how to safely override the superclass's methods and when it is safe to call them. The technique consists of a set of rules and some new forms of specification. Part of the specification would be generated automatically by a tool, a prototype of which is planned for the formal specification language JML. We give an example to show the kinds of problems caused by method overrides and how our technique can be used to avoid them. We also argue why the technique is sound and give guidelines for library providers and programmer...

Many popular object-oriented programming languages, such as C++, Smalltalk-80, Java, and Eiffel, do not support multiple dispatch. Yet without multiple dispatch, programmers find it difficult to express binary methods and design patterns such as the "visitor" pattern. We describe a new, simple, and orthogonal way to add multimethods to single-dispatch object-oriented languages, without affecting existing code. The new mechanism also clarifies many differences between single and multiple dispatch.

Abstract. 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.

Two major obstacles that hinder the wider acceptance of multimethods are (1) concerns over the lack of encapsulation and modularity and (2) the absence of static typechecking in existing multimethod-based languages.This article addresses both of these problems.We present a polynomial-time, static typechecking algorithm that checks the conformance, completeness, and consistency of a group of method implementations with respect to declared message signatures.This algorithm improves on previous algorithms by handling separate type and inheritance hierarchies, abstract classes, and graph-based method lookup semantics.We also present a module system that enables independently developed code to be fully encapsulated and statically typechecked on a per-module basis.To guarantee that potential conflicts between independently developed modules have been resolved, a simple well-formedness condition on the modules comprising a program is checked at link-time.The typechecking algorithm and module system are applicable to a range of multimethod-based languages, but the article uses the Cecil language as a concrete example of how they can be applied.

Two major obstacles hindering the wider acceptance of multi-methods are concerns over the lack of encapsulation and modularity and the absence of static typechecking in existing multi-method-based languages. This paper addresses both of these problems. We present a polynomial-time static typechecking algorithm that checks the conformance, completeness, and consistency of a group of method implementations with respect to declared message signatures. This algorithm improves on previous algorithms by handling separate type and inheritance hierarchies, abstract classes, and graph-based method lookup semantics. We also present a module system that enables independently-developed code to be fully encapsulated and statically typechecked on a per-module basis. To guarantee that potential conflicts between independently-developed modules have been resolved, a simple well-formedness condition on the modules comprising a program is checked at link-time. The typechecking algorithm and module system are applicable to a range of multi-method-based languages, but the paper uses the Cecil language as a concrete example of how they can be applied.

Object-oriented programming languages, such as Smalltalk, help one to build reusable program modules. The reuse of program modules requires adequate documentation --- formal or informal. Larch/Smalltalk is a formal specification language for specifying such reusable Smalltalk modules. Larch/Smalltalk firmly separates specification from implementation. In Larch/Smalltalk, the unit of specification is an abstract data type, which is an abstraction of the behavior produced by one or more Smalltalk classes. A type can be a subtype of other types, which allows types to be organized based on specified behavior, and also allows for inheritance of their specifications. Larch/Smalltalk specifications are developed using specification tools integrated in the Smalltalk programming environment.

Article Free Access Share on Formal techniques for OO software development Authors: Pierre America Philips Research Laboratories Philips Research LaboratoriesView Profile , Derek Coleman HP-Lab Bristol HP-Lab BristolView Profile , Roger Duke University of Queensland University of QueenslandView Profile , Doug Lea Syracuse University & SUNY-Oswego Syracuse University & SUNY-OswegoView Profile , Gary Leavens Iowa State University Iowa State UniversityView Profile Authors Info & Claims OOPSLA '91: Conference proceedings on Object-oriented programming systems, languages, and applicationsNovember 1991 Pages 166–170https://doi.org/10.1145/117954.117967Published:01 November 1991Publication History 2citation376DownloadsMetricsTotal Citations2Total Downloads376Last 12 Months13Last 6 weeks1 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