Automated Debugging In Java Using OCL And JDI

The different activities related to debugging such as program instrumentation, representation of execution trace and analysis of trace are not typically performed in an unified framework. We propose \textit{BOLD}, an Ontology-based Log Debugger to unify and standardize the activities in debugging. The syntactical information of programs can be represented in the from of Resource Description Framework (RDF) triples. Using the BOLD framework, the programs can be automatically i...

This paper summarizes our experience in communicating the elements of reasoning about correctness, and the central role of formal specifications in reasoning about modular, component-based software using a language and an integrated Web IDE designed for the purpose. Our experience in using such an IDE, supported by a 'push-button' verifying compiler in a classroom setting, reveals the highly iterative process learners use to arrive at suitably specified, automatically provabl...

In this paper we present a possible way how a precise semantics of object oriented modeling techniques can be achieved and what the possible benefits are .We outline the main modeling techniques used in the SysLab project sketch how a precise semantics can be given and how this semantics can be used during the development process.

The Object Constraint Language (OCL) has been widely used in the modeling community to complement software models for precisely defining constraints and business rules for the modeled systems. There is a limited number of tools supporting the definition and interpretation of OCL constraints, even less for a Python-based modelling approaches. In this paper, we introduce an OCL interpreter for Python. The interpreter has two components: parser and evaluator. We implement the ...

Automatic program verification has made tremendous strides, but is not yet for the masses. How do we make it less painful? This article addresses one of the obstacles: the need to specify explicit "frame clauses", expressing what properties are left unchanged by an operation. It is fair enough to ask the would-be (human) prover to state what each operation changes, and how, but the (mechanical) prover also requires knowledge of what it does not change. The process of specifyi...

Design by Contract enables seamless software development by unifying software requirements with their implementations. In its pure form, however, Design by Contract leaves some problems with contracts' expressiveness, verifiability, and reusability open. These problems significantly reduce practical applicability of seamless development. The present article introduces seamless object-oriented requirements - a novel approach to seamless development that builds upon Design by C...

This paper describes a new modelling language for the effective design of Java annotations. Since their inclusion in the 5th edition of Java, annotations have grown from a useful tool for the addition of meta-data to play a central role in many popular software projects. Usually they are conceived as sets with dependency and integrity constraints within them; however, the native support provided by Java for expressing this design is very limited. To overcome its deficiencies ...

This paper summarizes our efforts to aid human reasoning when verification fails through the use of two distinct Formalization Integrated Development Environments (F-IDEs) that we have developed. Both environments are modular and facilitate reasoning about the full behavior of object-based code. The first environment, referred to as the web-IDE, has been used for several years to teach aspects of formal specification and verification, including why and where verification cond...

Domain-specific debugging visualizations try to provide a view of a runtime object tailored to a specific domain and highlighting its important properties. The research in this area has focused mainly on the technical aspects of the creation of such views so far. However, we still lack answers to questions such as what properties of objects are considered important for these visualizations, whether all objects have an appropriate domain-specific view, or what clues could help...

Bug localization in object oriented program ha s always been an important issue in softeware engineering. In this paper, I propose a source level bug localization technique for object oriented embedded programs. My proposed technique, presents the idea of debugging an object oriented program in class level, incorporating the object state information into the Class Dependence Graph (ClDG). Given a program (having buggy statement) and an input that fails and others pass, my app...