Faraz Hussain · 2009
Specification languages help programmers write correct programs and also aid efforts for dynamically checking a software implementation with respect to its desired specifications. Most mainstream specification languages primarily deal with a program’s functional behavior. However, for certain applications it is more natural and intuitive to be able to express a system’s temporal properties. This thesis enhances the capabilities of the Java Modeling Language (JML), a behavioral interface specification language, by incorporating temporal logic constructs. The temporal specification grammar used is a modification of the JML temporal extension proposed by K. Trentelman and M. Huisman in their paper “Extending JML Specifications with Temporal Logic”. I have modified jmlc, the runtime assertion checker for the Java Modeling Language, so that it also generates runtime assertion checking code to dynamically check a program’s temporal specifications.
Cited by 1Open access
C. Marche, C. Paulin-mohring, X. Urbain · 2003
We describe the basic structure of an environment for proving Java programs annotated with JML specications. Our method is generic with respect to the API, and thus well suited for JavaCard applets certication. It involves three distinct components: the Why tool, which computes proof obligations for a core imperative language annotated with pre- and post-conditions, the Coq proof assistant for modeling the program semantics and conducting the development of proofs, and nally the Krakatoa tool, a translator of our own, which reads the Java les and produces specications for Coq and a representation of the semantics of the Java program into Why's input language.
Cited by 0
Marieke Huisman · Radboud Repository (Radboud University) · 2001
This thesis describes the first steps of a project aimed at formal verification of Java programs. The work presented here is part of a larger project called LOOP, for Logic of Object Oriented Programming. A semantics for Java is described in type theory and it is shown how this semantics forms the basis for program verification. The verifications are done with the use of interactive theorem provers,namely PVS and Isabelle. Both theorem provers are described in some detail, resulting in a comparison of the strong and weak points of both systems. A Hoare logic is discussed, which is especially tailored to reasoning about Java. The LOOP project resulted in the construction of the so-called LOOP compiler, which takes Java classes as input and returns PVS or Isabelle theories, capturing the semantics of the Java program, as output. This thesis also briefly describes a specification language for Java, called JML (Java modeling language). This language can be used to specify Java classes.Finally, two non-trivial case studies are described in this thesis, verifying properties of standard Java library classes. The first case study verifies a class invariant over class Vector, the second case study verifies the functional behaviour of the class AbstractCollection
Cited by 64Open access
Anna Armentrout · 1999
This project intends to develop a simple UML (Unified Modeling Language) tool in Java to be used by students learning object-oriented design and Java programming. Each student will be able to design a Java program by filling in forms (use cases, CRC cards) and making diagrams (use case diagrams, class diagrams and sequence diagrams) in a number of views. When the student enters information for any one of the views the tool will update the equivalent information for the other views. The tool will generate Java skeleton code from information supplied by the student.
Cited by 1Open access
Ulrich Kaiser · 2001
Java, known from web pages (applets), is also useful for design of application programs. This paper presents how the object-orientated language Java makes modeling and simulation of electronic circuits and systems possible, resulting in a portable program containing a graphical user interface as well. Customer demos by fast prototyping and executable specifications can be built by means of this method.
Cited by 0
Sean Thompson · 1999
Due to the recent advancements of the Internet, Java has become a dominant programming language, especially for coding concurrent applications. Finite state verification is a powerful technique for detecting subtle errors in a program. This paper reviews recent attempts to transform Java source code into a model that can be checked using verification tools. Two classes of techniques are reviewed. The first is translating Java source code into a known modeling language such as Promela. The second is building a finite state model based on the source and performing state reductions. Once state reductions are performed and the model size reduced, the resulting model can be checked for desired properties.
Cited by 0
Bart Jacobs, Martijn Warnier · 2007
In this paper we introduce two new ways of establishing confidentiality for sequential Java source code. The first one uses a functional formulation of confidentiality, in what we call a specification pattern in the Java Modeling Language JML. It is based on earlier work of Joshi and Leino, and can be proven via standard program verification techniques. Because of limitations in this approach...
Cited by 0
Cees-Bart Breunesse, Erik Poll · 2003
The specification language JML (Java Modeling Language) provides model fields as a means to abstract away from implementation details in specifications. This paper investigates how specifications with model fields can be translated to proof obligations. In order to do this, the semantics of model fields has to be made precise.
Cited by 0
Henrique Rebêlo, Ricardo Lima, Mrcio L. Cornlio · 2012
The Java Modeling Language (JML) is a formal interface specification language designed for Java. It was developed with the aim of improving the functional software correctness of Java applications. JML has a rich set of features for specifying Java applications, including abstract specifications, method and type specifications, and multiple inheritance specifications. The current JML compiler (jmlc) does not work properly when applied to Java dialects such as Java ME. The instrumented code generated by the original JML compiler uses the Java reflection mechanism and data structures not supported by Java ME platform. In order to overcome this limitation, our new JML compiler --- ajmlc (AspectJ JML Compiler) --- uses AspectJ to instrument Java code with JML contracts. A set of translation rules are defined from JML contracts into AspectJ program code. The result is a code compliant with both Java SE and Java ME applications. The translation rules handle a number of JML specifications, such as pre-, postconditions, and invariants. This book also includes proofs of concept to compare the size of the final code generated by our compiler with the code size produced by the jmlc compiler.
Cited by 0
Dwight Deugo, Dwight Deugo, Richard Deadman et al. · Cambridge University Press eBooks · 2000
More Java Gems presents the best articles and columns published in Java Report between 1997 and 1999. Dwight Deugo, Editor of Java Report, has carefully selected each article to be independent of any specific version of Java. The material relies mainly on those classes that are now part of the standard Java class library and APIs. Also, each article and column discusses Java topics and implementations that are not readily available in a single book. The book serves as an excellent reference to anyone involved with Java. The reader can learn more about the language, perform analysis, design and modeling, work on specific implementations, check performance, and perform testing. This book presents the good ideas of people who have used Java for 'real' applications.
Cited by 5
C. R. Russell, R. G. Dewar · 2008
This paper introduces an XML encoded reverse engineering transformation from Java to the Unified Modeling Language (UML). We explore the relationship between an XML based representation of Java, namely JavaML, and an XML based representation of UML, XMI. A series of XSLT templates are then described that reverse engineer Java to UML Class diagrams. By exploiting XML technologies, this approach demonstrates the opportunities for simple, standardised and adaptable conversions between code and design information, within a software development and maintenance environment. 1.
Cited by 0
Ramírez-de León Edgar Darío, Chávez-Bosquez Oscar, Francisco-León Julián Javier · SHILAP Revista de lepidopterología · 2014
XJML (Ramírez et al., 2012) is a modular external platform for Verification and Validation of Java classes using the Java Modeling Language (JML) through contracts written in XML. One problem faced in the XJML development was how to integrate Full Static Program Verification (FSPV). This paper presents the experiments and results that allowed us to define what tool to embed in XJML to execute FSPV.
Cited by 0Open access
Enea, Andrei · Zenodo (CERN European Organization for Nuclear Research) · 2024
This paper presents a framework to improve the reliability of Large Language Models (LLMs) in code generation by integrating formal programming language properties into the decoding process. The proposed methods—Syntax-Guided Generation (SGG) and Type-Aware Generation (TAG)—use grammars and static type checking to ensure syntactic and semantic correctness in Java code. Experiments on HumanEval, MBPP, CodexGLUE, and a custom Java dataset show that syntax guidance reduces invalid code by up to 24%, type-aware constraints improve semantic accuracy by up to 22%, and combined methods boost functional correctness by up to 15%. This work bridges statistical language modeling and formal language theory, demonstrating that constraint-based generation enhances LLM code reliability.
Cited by 0Open access
Manokar Munisamy · KTH Publication Database DiVA (KTH Royal Institute of Technology) · 2014
The current OpenModelica Complier (OMC) translates Modelica models into executable Ccodethrough several stages. The Code Generator is the final stage of the compiler whichgenerates target C-code from the optimized sorted equations. Recently, the Code Generator inOMC has been rewritten using the OpenModelica text template language. This gives a moreconcise and easier to understand code generator. Modeling and simulation is becomingincreasingly used in several application areas. There is demand for the OpenModelicaComplier (OMC) to generate code in languages like C#, CSharp, XML, JAVA and so on. Inthis thesis work, we implement a Java code generator to translate the internal equation-basedmodels in OpenModelica and its extension MetaModelica into a Java code representation. Tocreate the Java code generator we used the OpenModelica text template language, also calledSusan. This work is an important step on the way to finalize a full version of a Java CodeGenerator for the OpenModelica Complier (OMC).
Cited by 0Open access
R.A. Kilgore · 2000 Winter Simulation Conference Proceedings (Cat. No.00CH37165) · 2002
Silk(R) is a set of Java classes that support object-oriented, general-purpose simulation and animation using the Java programming language. Silk enables the development of complex, yet manageable simulations through the construction of usable and reusable simulation objects. Silk objects are usable because they express the precise behavior of individual entity-threads from the object perspective using familiar process-oriented modeling constructs and the object-oriented features of a general purpose programming language. Silk objects are reusable because they can be easily archived, edited and assembled using professional Java visual development environments that support the JavaBeans component architecture. This introduction describes the fundamentals of designing and creating a Silk model.
Cited by 12
David R. Cok · 2008
Despite the current effort to implement the Java Modeling Language for Java 1.5, and in particular for generic types, there has been no analysis of the effect of such a transition on JML itself, nor of what language changes should be implemented to take best advantage of the features of current Java. This paper analyzes the interactions between JML and the new features of Java 1.5 and 1.6, and it proposes appropriate changes to JML. Many implementation details for JML tools can be handled by choosing an existing Java 1.5+ compiler as a base; however, there are adjustments to the typing of JML expressions that would be appropriate, and there are issues needing careful attention arising from refinements, autoboxing, lock ordering operations, specification of enhanced for loops, type erasure, and the runtime execution of specifications involving type parameters. The features are implemented experimentally in
Cited by 12
Klaus Bergner, Andreas Rausch, Marc Sihling · 1998
The Unified Modeling Language consists of a set of mostly graphical description techniques for the specification, modeling, and documentation of object-oriented systems. Based on the experience gained in using UML 1.0 for the development of a medium-sized, distributed Java program, we comment on its strengths and weaknesses. Furthermore, some proposals for extensions and changes are made.
Cited by 7
Rohit Gheyi, Paulo Borba · Electronic Notes in Theoretical Computer Science · 2004
This paper proposes modeling laws for Alloy, a formal object-oriented modeling language. These laws are important not only to define the axiomatic semantics of Alloy but also to guide and formalize popular software development practices. In particular, these laws can be used to formaly refactor specifications. As an example, we formally refactor a specification for Java types.
Cited by 14Open access
Sanjar Erdolatov · 2011
In this paper the ObjectIF for students provided in teaching programming languages at higher education with applications in Java and how it is modeled with UML (Unified Modeling Language). Functions, advantages, disadvantages and basic ideas of the ObjectIF are given.
Cited by 1
Aimin Wang, Jipeng Wang, Zhe Zhao · 2008
The Vendition Management System (VMS) is designed basing on WEB and J2EE. The Java programming language, XML, Internet/Intranet and the Unified Modeling Language (UML) are used in the development of the system. The object oriented software project developing model (OOA/OOD/OOP) and the professional project managing method (RUP/XP) are also involved in the project.
Cited by 0