We introduce a generic type system for featherweight java (FJ) that is parametrized with a monad-like structure, and prove a uniform soundness theorem. Its instances include some region type systems studied by Martin ...
详细信息
ISBN:
(纸本)9781450385435
We introduce a generic type system for featherweight java (FJ) that is parametrized with a monad-like structure, and prove a uniform soundness theorem. Its instances include some region type systems studied by Martin Hofmann et al. as well as a new one that performs more precise analysis of trace-based properties. Their soundness is guaranteed by the uniform theorem. We only need to verify some natural conditions. Instead of refining the FJ type system as in the previous work, our region type system is separate from the FJ type system, making it simpler and also easier to move to larger fragments of java. Moreover, the uniform framework helps to avoid redundant work on the meta-theory when extending the system to cover other language features such as exception handling.
featherweight java is one of the most popular calculi which specify object-oriented programming features. It has been used as the basis for investigating novel language functionalities, as well as to specify and under...
详细信息
ISBN:
(纸本)9781450376389
featherweight java is one of the most popular calculi which specify object-oriented programming features. It has been used as the basis for investigating novel language functionalities, as well as to specify and understand the formal properties of existing features for languages in this paradigm. However, when considering mechanized formalization, it is hard to find an implementation for languages with complex structures and binding mechanisms as featherweight java. In this paper we explore an inherently-typed approach to formalize featherweight java, implementing the static and dynamic semantics in Agda using dependent types, and then replicating it in Coq (the latter using the Equations plug-in). Using this approach, the interpreter is correct by construction, since the type checker of the host language is responsible for verifying type safety, thus avoiding repetitions of proofs and error checking.
Currently, java is one of the most used programming language, being adopted in many large projects, where applications reach a level of complexity for which manual testing and human inspection are not enough to guaran...
详细信息
Currently, java is one of the most used programming language, being adopted in many large projects, where applications reach a level of complexity for which manual testing and human inspection are not enough to guarantee quality in software development. Even when using automated unit tests, such tests rarely cover all interesting cases of code, which means that a bug could never be discovered, once the code is tested against the same set of rules over and over again. This paper addresses the problem of generating random well-typed programs in the context of featherweight java, a well-known object-oriented calculus, using QuickCheck, a Haskell library for property-based testing.
Currently, java is one of the most used programming language, being adopted in many large projects, where applications reach a level of complexity for which manual testing and human inspection are not enough to guaran...
详细信息
Currently, java is one of the most used programming language, being adopted in many large projects, where applications reach a level of complexity for which manual testing and human inspection are not enough to guarantee quality in software development. Even when using automated unit tests, such tests rarely cover all interesting cases of code, which means that a bug could never be discovered, once the code is tested against the same set of rules over and over again. This paper addresses the problem of generating random well-typed programs in the context of featherweight java, a well-known object-oriented calculus, using QuickCheck, a Haskell library for property-based testing.
Nowadays, several languages and libraries have been proposed to program and reason about quantum programs in the imperative and functional paradigms. Although the object-oriented paradigm is one of the most used for g...
详细信息
ISBN:
(数字)9783319452791
ISBN:
(纸本)9783319452791;9783319452784
Nowadays, several languages and libraries have been proposed to program and reason about quantum programs in the imperative and functional paradigms. Although the object-oriented paradigm is one of the most used for general purpose software, there is a lack of quantum programming languages designed with this paradigm in mind. In this paper, we present the monadic semantics for FJQuantam, an object-oriented language based on featherweight java, created to reason and to develop programs handling quantum data and quantum operations, taking advantage of the characteristics of that paradigm. We also show a set of examples of quantum programs using the proposed language.
We consider semantics for the class-based object-oriented calculus featherweight java (without casts) based upon approximation. We also define an intersection type assignment system for this calculus and show that it ...
详细信息
We consider semantics for the class-based object-oriented calculus featherweight java (without casts) based upon approximation. We also define an intersection type assignment system for this calculus and show that it satisfies subject reduction and expansion, i.e. types are preserved under reduction and its converse. We establish a link between type assignment and the approximation semantics by showing an approximation result, which leads to a sufficient condition for the characterisation of head-normalisation and termination. We show the expressivity of both our calculus and our type system by defining an encoding of Combinatory Logic into our calculus and showing that this encoding preserves typeability. We also show that our system characterises the normalising and strongly normalising terms for this encoding. We thus demonstrate that the great analytic capabilities of intersection types can be applied to the context of class-based object orientation. (C) 2013 Elsevier B.V. All rights reserved.
We present FJ &lambda star, a new core calculus that extends featherweight java (FJ) with interfaces, lambda-expressions, intersection types and a form of dynamic type. Intersection types can be used anywhere, in ...
详细信息
ISBN:
(纸本)9798400702464
We present FJ &lambda star, a new core calculus that extends featherweight java (FJ) with interfaces, lambda-expressions, intersection types and a form of dynamic type. Intersection types can be used anywhere, in particular to specify target types of lambda-expressions. The dynamic type is exploited to specify parts of the class tables and programs we want to exclude temporarily from static typing. Our main result is the gradual guarantee, which says that if a program is well typed in a class table, then replacing type annotations (from the program and from the class table) with the dynamic type always produces a program that is still well typed in the obtained class table. Furthermore, if a typed program evaluates to a value in a class table, then replacing type annotations with dynamic types always produces a program that evaluates to the same value in the obtained class table.
Region-based type systems are a powerful tool for various kinds of program analysis. We introduce a new inference algorithm for region types based on an abstract notion of environment transformation. It analyzes the c...
详细信息
ISBN:
(纸本)9783031210365;9783031210372
Region-based type systems are a powerful tool for various kinds of program analysis. We introduce a new inference algorithm for region types based on an abstract notion of environment transformation. It analyzes the code of a method only once, even when there are multiple invocations of the method of different region types in the program. Elements of such an abstract transformation are essentially constraints for equality and subtyping that capture flow information of the program. In particular, we work with access graphs in the definition of abstract transformations to guarantee the termination of the inference algorithm, because they provide a finite representation of field access paths.
A common approach to improve software quality is to use programming guidelines to avoid common kinds of errors. In this paper, we consider the problem of enforcing guidelines for featherweight java (FJ). We formalize ...
详细信息
ISBN:
(纸本)9781450386890
A common approach to improve software quality is to use programming guidelines to avoid common kinds of errors. In this paper, we consider the problem of enforcing guidelines for featherweight java (FJ). We formalize guidelines as sets of finite or infinite execution traces and develop a region-based type and effect system for FJ that can enforce such guidelines. We build on the work by Erbatur, Hofmann and Zalinescu, who presented a type system for verifying the finite event traces of terminating FJ programs. We refine this type system, separating region typing from FJ typing, and use ideas of Hofmann and Chen to extend it to capture also infinite traces produced by non-terminating programs. Our type and effect system can express properties of both finite and infinite traces and can compute information about the possible infinite traces of FJ programs. Specifically, the set of infinite traces of a method is constructed as the greatest fixed point of the operator which calculates the possible traces of method bodies. Our type inference algorithm is realized by working with the finitary abstraction of the system based on Buchi automata.
Property-based testing of compilers or programming language semantics is difficult to accomplish because it is hard to design a random generator for valid programs. Most compiler test tools do not have a well-specifie...
详细信息
Property-based testing of compilers or programming language semantics is difficult to accomplish because it is hard to design a random generator for valid programs. Most compiler test tools do not have a well-specified way for generating type-correct programs, which is a requirement for such testing activities. In this project, we formalize a type-directed procedure to generate random well-typed java 8 programs in the context of featherweight java, extending it with interfaces, lambda-expressions and default methods. We implement the approach using the Haskell programming language and verify it against relevant properties using QuickCheck, a library for property-based testing. (C) 2020 Elsevier B.V. All rights reserved.
暂无评论