| 1. |
- Hedin, Görel, et al.
(author)
-
JastAdd - an aspect-oriented compiler construction system
- 2003
-
In: Science of Computer Programming. - 0167-6423. ; 47:1, s. 37-58
-
Journal article (peer-reviewed)abstract
- We describe JastAdd, a Java-based system for compiler construction. JastAdd is centered around an object-oriented representation of the abstract syntax tree where reference variables can be used to link together different parts of the tree. JastAdd supports the combination of declarative techniques (using Reference Attributed Grammars) and imperative techniques (using ordinary Java code) in implementing the compiler. The behavior can be modularized into different aspects, e.g. name analysis, type checking, code generation, etc., that are woven together into classes using aspect-oriented programming techniques, providing a safer and more powerful alternative to the Visitor pattern. The JastAdd system is independent of the underlying parsing technology and supports any noncircular dependencies between computations, thereby allowing general multi-pass compilation. The attribute evaluator (optimal recursive evaluation) is implemented very conveniently using Java classes, interfaces, and virtual methods. (C) 2002 Elsevier Science B.V. All rights reserved.
|
|
| 2. |
- Jansson, Patrik, 1972, et al.
(author)
-
Polytypic Data Conversion Programs
- 2002
-
In: Science of Computer Programming. - 0167-6423. ; 43:1, s. 35-75
-
Journal article (peer-reviewed)abstract
- Several generic programs for converting values from regular datatypes to some other format, together with their corresponding inverses, are constructed. Among the formats considered are shape plus contents, compact bit streams and pretty printed strings. The different data conversion programs are constructed using John Hughes arrow combinators along with a proof that printing (from a regular datatype to another format) followed by parsing (from that format back to the regular datatype) is the identity. The printers and parsers are described in PolyP, a polytypic extension of the functional language Haskell.
|
|
| 3. |
- Nordlander, Johan
(author)
-
Polymorphic subtyping in O'Haskell
- 2002
-
In: Science of Computer Programming. - 0167-6423 .- 1872-7964. ; 43:2-3, s. 93-127
-
Journal article (peer-reviewed)abstract
- O'Haskell is a programming language derived from Haskell by the addition of concurrent reactive objects and subtyping. Because Haskell already encompasses an advanced type system with polymorphism and overloading, the type system of O'Haskell is much richer than what is the norm in almost any widespread object-oriented or functional language. Yet, there is strong evidence that O'Haskell is not a complex language to use, and that both Java and Haskell programmers can easily find their way with its polymorphic subtyping system. This paper describes the type system of O'Haskell both formally and from a programmer's point of view; the latter task is accomplished with the aid of an illustrative, real-world programming example: a strongly typed interface to the graphical toolkit Tk.
|
|
| 4. |
- Abd Alrahman, Yehia, 1986, et al.
(author)
-
Programming interactions in collective adaptive systems by relying on attribute-based communication
- 2020
-
In: Science of Computer Programming. - : Elsevier BV. - 0167-6423. ; 192:June
-
Journal article (peer-reviewed)abstract
- © 2020 Elsevier B.V. Collective adaptive systems are new emerging computational systems consisting of a large number of interacting components and featuring complex behaviour. These systems are usually distributed, heterogeneous, decentralised and interdependent, and are operating in dynamic and possibly unpredictable environments. Finding ways to understand and design these systems and, most of all, to model the interactions of their components, is a difficult but important endeavour. In this article we propose a language-based approach for programming the interactions of collective-adaptive systems by relying on attribute-based communication; a paradigm that permits a group of partners to communicate by considering their run-time properties and capabilities. We introduce AbC, a foundational calculus for attribute-based communication and show how its linguistic primitives can be used to program a sophisticated variant of the well-known problem of Stable Allocation in Content Delivery Networks. In our variant, content providers are assigned to clients based on collaboration and by taking into account the preferences of both parties in a fully anonymous and distributed settings. We also illustrate the expressive power of attribute-based communication by showing the natural encoding of group-based, publish/subscribe-based and channel-based communication paradigms into AbC.
|
|
| 5. |
- Aceto, Luca, et al.
(author)
-
Rule formats for determinism and idempotence
- 2012
-
In: Science of Computer Programming. - Amsterdam : Elsevier BV. - 0167-6423 .- 1872-7964. ; 77:7-8, s. 889-907
-
Journal article (peer-reviewed)abstract
- Determinism is a semantic property of (a fragment of) a language that specifies that a program cannot evolve operationally in several different ways. Idempotence is a property of binary composition operators requiring that the composition of two identical specifications or programs will result in a piece of specification or program that is equivalent to the original components. In this paper, we propose (related) meta-theorems for guaranteeing the determinism and idempotence of binary operators. These meta-theorems are formulated in terms of syntactic templates for operational semantics, called rule formats. In order to obtain a powerful rule format for idempotence, we make use of the determinism of certain transition relations in the definition of the format for idempotence. We show the applicability of our formats by applying them to various operational semantics from the literature.
|
|
| 6. |
- Ahrendt, Wolfgang, 1967, et al.
(author)
-
A System for Compositional Verification of Asynchronous Objects
- 2012
-
In: Science of Computer Programming. - : Elsevier BV. - 0167-6423. ; 77:12, s. 1289-1309
-
Journal article (peer-reviewed)abstract
- We present a semantics, calculus, and system for compositional verification of Creol, an object-oriented modelling language for concurrent distributed applications. The system is an instance of KeY, a framework for object oriented software verification, which has so far been applied foremost to sequential Java. Building on KeY characteristic concepts, like dynamic logic, sequent calculus, symbolic execution via explicit substitutions, and the taclet rule language, the presented system addresses functional correctness of Creol models featuring local cooperative thread parallelism and global communication via asynchronous method calls. The calculus heavily operates on communication histories specified by the interfaces of Creol units. Two example scenarios demonstrate the usage of the system. This article extends the conference paper of Ahrendt and Dylla (2009) with a denotational semantics of Creol and an assumption-commitment style semantics of the logic.
|
|
| 7. |
- Aktug, Irem, et al.
(author)
-
ConSpec : A Formal Language for Policy Specification
- 2008
-
In: Science of Computer Programming. - : Elsevier BV. - 0167-6423 .- 1872-7964. ; 74:1-2, s. 2-12
-
Journal article (peer-reviewed)abstract
- The paper presents ConSpec, an automata-based policy specification language. The language trades off clean semantics to language expressiveness: a formal semantics for the language is provided as security automata. ConSpec specifications can be used at different stages of the application lifecycle, rendering possible the formalization of various Policy enforcement techniques.
|
|
| 8. |
- Araujo, Hugo, et al.
(author)
-
Sound conformance testing for cyber-physical systems : Theory and implementation
- 2018
-
In: Science of Computer Programming. - Amsterdam : ELSEVIER SCIENCE BV. - 0167-6423 .- 1872-7964. ; 162, s. 35-54
-
Journal article (peer-reviewed)abstract
- Conformance testing is a formal and structured approach to verifying system correctness. We propose a conformance testing algorithm for cyber-physical systems, based on the notion of hybrid conformance by Abbas and Fainekos. We show how the dynamics of system specification and the sampling rate play an essential role in making sound verdicts. We specify and prove error bounds that lead to sound test-suites for a given specification and a given sampling rate. We use reachability analysis to find such bounds and implement the proposed approach using the CORA toolbox in Matlab. We apply the implemented approach on a case study from the automotive domain.
|
|
| 9. |
|
|
| 10. |
|
|
