FTfJP '22: "On the Need for a Common API ..."
On the Need for a Common API for Abstract Domains of Object-Oriented Programs
Gianluca Amato, Maria Chiara Meo, and Francesca Scozzari
(Università di Chieti-Pescara, Italy)
In the last years almost all families of programming languages, from imperative to functional, logic, object-oriented and machine code, have been subject to static analysis by abstract interpretation. The use of a principled approach to static analysis based on the theory of abstract interpretation provided mathematical tools to reason about program properties and allowed for the rigorous and incremental design of precise and scalable static analyzers, ensuring soundness by construction. The large variety of abstract domains for many different programming languages, the ability to combine and refine them with standard abstract interpretation tools and the availability of mature abstract domain libraries allowed easily porting, reusing and experimenting with techniques born in a specific family to other programming languages and properties.
Since the use of abstract interpretation for the analysis of object-oriented languages is less common than in other application fields of static analysis, in order to increase its adoption, we advocate the need to establish a common interface for designing and implementing abstract domains for the static analysis of Java-like programs. This interface should allow developing abstract domains pluggable in a generic abstract interpreter, as it is customary, for example, in abstract interpretation-based static analysis of numerical properties.
@InProceedings{FTfJP22p15,
author = {Gianluca Amato and Maria Chiara Meo and Francesca Scozzari},
title = {On the Need for a Common API for Abstract Domains of Object-Oriented Programs},
booktitle = {Proc.\ FTfJP},
publisher = {ACM},
pages = {15--17},
doi = {10.1145/3611096.3611100},
year = {2022},
}
Publisher's Version
FTfJP '22: "Automated Reasoning Repair ..."
Automated Reasoning Repair
Amirfarhad Nilizadeh, Gary T. Leavens, and David R. Cok
(University of Central Florida, USA; Safer Software Consulting, USA)
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.
@InProceedings{FTfJP22p11,
author = {Amirfarhad Nilizadeh and Gary T. Leavens and David R. Cok},
title = {Automated Reasoning Repair},
booktitle = {Proc.\ FTfJP},
publisher = {ACM},
pages = {11--14},
doi = {10.1145/3611096.3611099},
year = {2022},
}
Publisher's Version
FTfJP '22: "Documentation and Educational ..."
Documentation and Educational Materials for a 2nd Edition of the Java Modeling Language
David R. Cok
(Safer Software Consulting, USA)
JML is an ambitious project in formal specification and verification, ongoing since 1997, that has aimed to bring value to Java programmers. Participants in the project are now undertaking a significant revision of the language itself (Cok, Leavens, Ulbrich) and accompanying that with educational materials (Cok, Meija, Leavens), documentation rewrites and tool upgrades (Cok). The current state of this work-in-progress is presented here in order to encourage wide-spread contribution and comment on the language revisions, its semantics, the educational tutorial, and related tools.
@InProceedings{FTfJP22p26,
author = {David R. Cok},
title = {Documentation and Educational Materials for a 2nd Edition of the Java Modeling Language},
booktitle = {Proc.\ FTfJP},
publisher = {ACM},
pages = {26--28},
doi = {10.1145/3611096.3611102},
year = {2022},
}
Publisher's Version
FTfJP '22: "A Graph-Based Formal Semantics ..."
A Graph-Based Formal Semantics of Reactive Programming from First Principles
Bjarno Oeyen, Joeri De Koster, and Wolfgang De Meuter
(Vrije Universiteit Brussel, Belgium)
In recent years, stream processing has become the de facto paradigm to process any kind of real-time data in many kinds of applications. Different libraries, frameworks and techniques exists which aim to make it easy to build stream processing applications in many modern programming languages…Libraries such as Reactive Extensions, Akka Streams, or web frameworks such as React and Vue are all based on the idea of data streams that model the flow of data in applications. To the best of our knowledge, there exist no formalism which captures the essential core semantics of these approaches in a straightforward, easy to understand, manner: namely its graph-based program structure and the way how values propagate through this graph. In this paper, we present Karcharias, a formalisation of reactive programming – a model that shares many core ideas found in the various aforementioned libraries and frameworks – that is built from first principles. Instead of extending an existing language with a graph-based stream processing framework, and formalising this integrated language, we formalised the reactive programming paradigm without relying on a base language (such as the λ-calculus). Using our formalism, we show how reactive programs (and thus, stream-based programs in general) need a way to construct a graph and to propagate events through that graph, even in the absence of a base language.
@InProceedings{FTfJP22p18,
author = {Bjarno Oeyen and Joeri De Koster and Wolfgang De Meuter},
title = {A Graph-Based Formal Semantics of Reactive Programming from First Principles},
booktitle = {Proc.\ FTfJP},
publisher = {ACM},
pages = {18--25},
doi = {10.1145/3611096.3611101},
year = {2022},
}
Publisher's Version
FTfJP '22: "A Graph-Based Formal Semantics ..."
A Graph-Based Formal Semantics of Reactive Programming from First Principles
Bjarno Oeyen, Joeri De Koster, and Wolfgang De Meuter
(Vrije Universiteit Brussel, Belgium)
In recent years, stream processing has become the de facto paradigm to process any kind of real-time data in many kinds of applications. Different libraries, frameworks and techniques exists which aim to make it easy to build stream processing applications in many modern programming languages…Libraries such as Reactive Extensions, Akka Streams, or web frameworks such as React and Vue are all based on the idea of data streams that model the flow of data in applications. To the best of our knowledge, there exist no formalism which captures the essential core semantics of these approaches in a straightforward, easy to understand, manner: namely its graph-based program structure and the way how values propagate through this graph. In this paper, we present Karcharias, a formalisation of reactive programming – a model that shares many core ideas found in the various aforementioned libraries and frameworks – that is built from first principles. Instead of extending an existing language with a graph-based stream processing framework, and formalising this integrated language, we formalised the reactive programming paradigm without relying on a base language (such as the λ-calculus). Using our formalism, we show how reactive programs (and thus, stream-based programs in general) need a way to construct a graph and to propagate events through that graph, even in the absence of a base language.
@InProceedings{FTfJP22p18,
author = {Bjarno Oeyen and Joeri De Koster and Wolfgang De Meuter},
title = {A Graph-Based Formal Semantics of Reactive Programming from First Principles},
booktitle = {Proc.\ FTfJP},
publisher = {ACM},
pages = {18--25},
doi = {10.1145/3611096.3611101},
year = {2022},
}
Publisher's Version
FTfJP '22: "Using Functional Reactive ..."
Using Functional Reactive Programming to Define Safe Actor Systems
Nick Webster, Marco Servetto, and Michael Homer
(Victoria University of Wellington, New Zealand)
Functional Reactive Programming (FRP) is a powerful abstraction for building deterministic concurrent systems. However, some programmers prefer a more imperative approach for certain tasks, and that approach is required to implement some imperative algorithms. The Actor Model provides an abstraction for building concurrent systems in a more imperative way without as much of the chaos typical of traditional shared-memory imperative concurrent programming. While the Actor Model offers more structure than other imperative approaches, it still suffers from nondeterminism due to message-ordering and processing times. That makes actor systems hard to reason about, limiting their effectiveness for critical tasks. We formally define an elegant multi-paradigm unification of event-driven FRP constructs and the Actor Model. Our unification enables an intuitive form of declarative programming that can integrate imperative and declarative code within each other. We use reference and object capabilities to tame imperative features: reference capabilities track aliasing and mutability, and object capabilities track I/O. Notably, in our system expressions with deeply immutable input behave deterministically. Additionally, capabilities provide a boundary to allow nondeterministic code to intermingle safely with deterministic code.
@InProceedings{FTfJP22p4,
author = {Nick Webster and Marco Servetto and Michael Homer},
title = {Using Functional Reactive Programming to Define Safe Actor Systems},
booktitle = {Proc.\ FTfJP},
publisher = {ACM},
pages = {4--10},
doi = {10.1145/3611096.3611098},
year = {2022},
}
Publisher's Version
FTfJP '22: "Formalizing 𝜑-Calculus: ..."
Formalizing 𝜑-Calculus: A Purely Object-Oriented Calculus of Decorated Objects
Nikolai Kudasov and Violetta Sim
(Innopolis University, Russian Federation)
Many calculi exist for modeling various features of object-oriented languages. Many of them are based on λ-calculus and focus either on statically typed class-based languages or dynamic prototype-based languages. We formalize the untyped calculus of decorated objects, informally presented by Bugayenko, which is defined in terms of objects and relies on decoration as a primary mechanism of object extension. It is not based on λ-calculus, yet with only four basic syntactic constructions is just as complete (in particular, it is Turing complete and possesses the Church-Rosser property). We also provide a sound translation to Wands’s λ-calculus with records and concatenation, and discuss the key differences of these calculi.
@InProceedings{FTfJP22p29,
author = {Nikolai Kudasov and Violetta Sim},
title = {Formalizing 𝜑-Calculus: A Purely Object-Oriented Calculus of Decorated Objects},
booktitle = {Proc.\ FTfJP},
publisher = {ACM},
pages = {29--36},
doi = {10.1145/3611096.3611103},
year = {2022},
}
Publisher's Version
FTfJP '22: "Automated Reasoning Repair ..."
Automated Reasoning Repair
Amirfarhad Nilizadeh, Gary T. Leavens, and David R. Cok
(University of Central Florida, USA; Safer Software Consulting, USA)
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.
@InProceedings{FTfJP22p11,
author = {Amirfarhad Nilizadeh and Gary T. Leavens and David R. Cok},
title = {Automated Reasoning Repair},
booktitle = {Proc.\ FTfJP},
publisher = {ACM},
pages = {11--14},
doi = {10.1145/3611096.3611099},
year = {2022},
}
Publisher's Version
FTfJP '22: "Rusty Links in Local Chains ..."
Rusty Links in Local Chains
James Noble, Julian Mackay, and Tobias Wrigstad
(Creative Research & Programming, New Zealand; Victoria University of Wellington, New Zealand; Uppsala University, Sweden)
Rust successfully applies ownership types to control memory allocation. Unfortunately, Rust's ownership restricts the programs' topologies to the point where doubly-linked lists cannot be programmed in Safe Rust. We sketch how more flexible "local" ownership could be added to Rust, permitting multiple mutable references to objects, provided each reference is bounded by the object's lifetime. To maintain thread-safety, locally owned objects must remain thread-local; to maintain memory safety, local objects must remain allocated until their owner's lifetime expires
@InProceedings{FTfJP22p1,
author = {James Noble and Julian Mackay and Tobias Wrigstad},
title = {Rusty Links in Local Chains},
booktitle = {Proc.\ FTfJP},
publisher = {ACM},
pages = {1--3},
doi = {10.1145/3611096.3611097},
year = {2022},
}
Publisher's Version
FTfJP '22: "On the Need for a Common API ..."
On the Need for a Common API for Abstract Domains of Object-Oriented Programs
Gianluca Amato, Maria Chiara Meo, and Francesca Scozzari
(Università di Chieti-Pescara, Italy)
In the last years almost all families of programming languages, from imperative to functional, logic, object-oriented and machine code, have been subject to static analysis by abstract interpretation. The use of a principled approach to static analysis based on the theory of abstract interpretation provided mathematical tools to reason about program properties and allowed for the rigorous and incremental design of precise and scalable static analyzers, ensuring soundness by construction. The large variety of abstract domains for many different programming languages, the ability to combine and refine them with standard abstract interpretation tools and the availability of mature abstract domain libraries allowed easily porting, reusing and experimenting with techniques born in a specific family to other programming languages and properties.
Since the use of abstract interpretation for the analysis of object-oriented languages is less common than in other application fields of static analysis, in order to increase its adoption, we advocate the need to establish a common interface for designing and implementing abstract domains for the static analysis of Java-like programs. This interface should allow developing abstract domains pluggable in a generic abstract interpreter, as it is customary, for example, in abstract interpretation-based static analysis of numerical properties.
@InProceedings{FTfJP22p15,
author = {Gianluca Amato and Maria Chiara Meo and Francesca Scozzari},
title = {On the Need for a Common API for Abstract Domains of Object-Oriented Programs},
booktitle = {Proc.\ FTfJP},
publisher = {ACM},
pages = {15--17},
doi = {10.1145/3611096.3611100},
year = {2022},
}
Publisher's Version
FTfJP '22: "Automated Reasoning Repair ..."
Automated Reasoning Repair
Amirfarhad Nilizadeh, Gary T. Leavens, and David R. Cok
(University of Central Florida, USA; Safer Software Consulting, USA)
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.
@InProceedings{FTfJP22p11,
author = {Amirfarhad Nilizadeh and Gary T. Leavens and David R. Cok},
title = {Automated Reasoning Repair},
booktitle = {Proc.\ FTfJP},
publisher = {ACM},
pages = {11--14},
doi = {10.1145/3611096.3611099},
year = {2022},
}
Publisher's Version
FTfJP '22: "Rusty Links in Local Chains ..."
Rusty Links in Local Chains
James Noble, Julian Mackay, and Tobias Wrigstad
(Creative Research & Programming, New Zealand; Victoria University of Wellington, New Zealand; Uppsala University, Sweden)
Rust successfully applies ownership types to control memory allocation. Unfortunately, Rust's ownership restricts the programs' topologies to the point where doubly-linked lists cannot be programmed in Safe Rust. We sketch how more flexible "local" ownership could be added to Rust, permitting multiple mutable references to objects, provided each reference is bounded by the object's lifetime. To maintain thread-safety, locally owned objects must remain thread-local; to maintain memory safety, local objects must remain allocated until their owner's lifetime expires
@InProceedings{FTfJP22p1,
author = {James Noble and Julian Mackay and Tobias Wrigstad},
title = {Rusty Links in Local Chains},
booktitle = {Proc.\ FTfJP},
publisher = {ACM},
pages = {1--3},
doi = {10.1145/3611096.3611097},
year = {2022},
}
Publisher's Version
FTfJP '22: "A Graph-Based Formal Semantics ..."
A Graph-Based Formal Semantics of Reactive Programming from First Principles
Bjarno Oeyen, Joeri De Koster, and Wolfgang De Meuter
(Vrije Universiteit Brussel, Belgium)
In recent years, stream processing has become the de facto paradigm to process any kind of real-time data in many kinds of applications. Different libraries, frameworks and techniques exists which aim to make it easy to build stream processing applications in many modern programming languages…Libraries such as Reactive Extensions, Akka Streams, or web frameworks such as React and Vue are all based on the idea of data streams that model the flow of data in applications. To the best of our knowledge, there exist no formalism which captures the essential core semantics of these approaches in a straightforward, easy to understand, manner: namely its graph-based program structure and the way how values propagate through this graph. In this paper, we present Karcharias, a formalisation of reactive programming – a model that shares many core ideas found in the various aforementioned libraries and frameworks – that is built from first principles. Instead of extending an existing language with a graph-based stream processing framework, and formalising this integrated language, we formalised the reactive programming paradigm without relying on a base language (such as the λ-calculus). Using our formalism, we show how reactive programs (and thus, stream-based programs in general) need a way to construct a graph and to propagate events through that graph, even in the absence of a base language.
@InProceedings{FTfJP22p18,
author = {Bjarno Oeyen and Joeri De Koster and Wolfgang De Meuter},
title = {A Graph-Based Formal Semantics of Reactive Programming from First Principles},
booktitle = {Proc.\ FTfJP},
publisher = {ACM},
pages = {18--25},
doi = {10.1145/3611096.3611101},
year = {2022},
}
Publisher's Version
FTfJP '22: "On the Need for a Common API ..."
On the Need for a Common API for Abstract Domains of Object-Oriented Programs
Gianluca Amato, Maria Chiara Meo, and Francesca Scozzari
(Università di Chieti-Pescara, Italy)
In the last years almost all families of programming languages, from imperative to functional, logic, object-oriented and machine code, have been subject to static analysis by abstract interpretation. The use of a principled approach to static analysis based on the theory of abstract interpretation provided mathematical tools to reason about program properties and allowed for the rigorous and incremental design of precise and scalable static analyzers, ensuring soundness by construction. The large variety of abstract domains for many different programming languages, the ability to combine and refine them with standard abstract interpretation tools and the availability of mature abstract domain libraries allowed easily porting, reusing and experimenting with techniques born in a specific family to other programming languages and properties.
Since the use of abstract interpretation for the analysis of object-oriented languages is less common than in other application fields of static analysis, in order to increase its adoption, we advocate the need to establish a common interface for designing and implementing abstract domains for the static analysis of Java-like programs. This interface should allow developing abstract domains pluggable in a generic abstract interpreter, as it is customary, for example, in abstract interpretation-based static analysis of numerical properties.
@InProceedings{FTfJP22p15,
author = {Gianluca Amato and Maria Chiara Meo and Francesca Scozzari},
title = {On the Need for a Common API for Abstract Domains of Object-Oriented Programs},
booktitle = {Proc.\ FTfJP},
publisher = {ACM},
pages = {15--17},
doi = {10.1145/3611096.3611100},
year = {2022},
}
Publisher's Version
FTfJP '22: "Using Functional Reactive ..."
Using Functional Reactive Programming to Define Safe Actor Systems
Nick Webster, Marco Servetto, and Michael Homer
(Victoria University of Wellington, New Zealand)
Functional Reactive Programming (FRP) is a powerful abstraction for building deterministic concurrent systems. However, some programmers prefer a more imperative approach for certain tasks, and that approach is required to implement some imperative algorithms. The Actor Model provides an abstraction for building concurrent systems in a more imperative way without as much of the chaos typical of traditional shared-memory imperative concurrent programming. While the Actor Model offers more structure than other imperative approaches, it still suffers from nondeterminism due to message-ordering and processing times. That makes actor systems hard to reason about, limiting their effectiveness for critical tasks. We formally define an elegant multi-paradigm unification of event-driven FRP constructs and the Actor Model. Our unification enables an intuitive form of declarative programming that can integrate imperative and declarative code within each other. We use reference and object capabilities to tame imperative features: reference capabilities track aliasing and mutability, and object capabilities track I/O. Notably, in our system expressions with deeply immutable input behave deterministically. Additionally, capabilities provide a boundary to allow nondeterministic code to intermingle safely with deterministic code.
@InProceedings{FTfJP22p4,
author = {Nick Webster and Marco Servetto and Michael Homer},
title = {Using Functional Reactive Programming to Define Safe Actor Systems},
booktitle = {Proc.\ FTfJP},
publisher = {ACM},
pages = {4--10},
doi = {10.1145/3611096.3611098},
year = {2022},
}
Publisher's Version
FTfJP '22: "Formalizing 𝜑-Calculus: ..."
Formalizing 𝜑-Calculus: A Purely Object-Oriented Calculus of Decorated Objects
Nikolai Kudasov and Violetta Sim
(Innopolis University, Russian Federation)
Many calculi exist for modeling various features of object-oriented languages. Many of them are based on λ-calculus and focus either on statically typed class-based languages or dynamic prototype-based languages. We formalize the untyped calculus of decorated objects, informally presented by Bugayenko, which is defined in terms of objects and relies on decoration as a primary mechanism of object extension. It is not based on λ-calculus, yet with only four basic syntactic constructions is just as complete (in particular, it is Turing complete and possesses the Church-Rosser property). We also provide a sound translation to Wands’s λ-calculus with records and concatenation, and discuss the key differences of these calculi.
@InProceedings{FTfJP22p29,
author = {Nikolai Kudasov and Violetta Sim},
title = {Formalizing 𝜑-Calculus: A Purely Object-Oriented Calculus of Decorated Objects},
booktitle = {Proc.\ FTfJP},
publisher = {ACM},
pages = {29--36},
doi = {10.1145/3611096.3611103},
year = {2022},
}
Publisher's Version
FTfJP '22: "Using Functional Reactive ..."
Using Functional Reactive Programming to Define Safe Actor Systems
Nick Webster, Marco Servetto, and Michael Homer
(Victoria University of Wellington, New Zealand)
Functional Reactive Programming (FRP) is a powerful abstraction for building deterministic concurrent systems. However, some programmers prefer a more imperative approach for certain tasks, and that approach is required to implement some imperative algorithms. The Actor Model provides an abstraction for building concurrent systems in a more imperative way without as much of the chaos typical of traditional shared-memory imperative concurrent programming. While the Actor Model offers more structure than other imperative approaches, it still suffers from nondeterminism due to message-ordering and processing times. That makes actor systems hard to reason about, limiting their effectiveness for critical tasks. We formally define an elegant multi-paradigm unification of event-driven FRP constructs and the Actor Model. Our unification enables an intuitive form of declarative programming that can integrate imperative and declarative code within each other. We use reference and object capabilities to tame imperative features: reference capabilities track aliasing and mutability, and object capabilities track I/O. Notably, in our system expressions with deeply immutable input behave deterministically. Additionally, capabilities provide a boundary to allow nondeterministic code to intermingle safely with deterministic code.
@InProceedings{FTfJP22p4,
author = {Nick Webster and Marco Servetto and Michael Homer},
title = {Using Functional Reactive Programming to Define Safe Actor Systems},
booktitle = {Proc.\ FTfJP},
publisher = {ACM},
pages = {4--10},
doi = {10.1145/3611096.3611098},
year = {2022},
}
Publisher's Version
FTfJP '22: "Rusty Links in Local Chains ..."
Rusty Links in Local Chains
James Noble, Julian Mackay, and Tobias Wrigstad
(Creative Research & Programming, New Zealand; Victoria University of Wellington, New Zealand; Uppsala University, Sweden)
Rust successfully applies ownership types to control memory allocation. Unfortunately, Rust's ownership restricts the programs' topologies to the point where doubly-linked lists cannot be programmed in Safe Rust. We sketch how more flexible "local" ownership could be added to Rust, permitting multiple mutable references to objects, provided each reference is bounded by the object's lifetime. To maintain thread-safety, locally owned objects must remain thread-local; to maintain memory safety, local objects must remain allocated until their owner's lifetime expires
@InProceedings{FTfJP22p1,
author = {James Noble and Julian Mackay and Tobias Wrigstad},
title = {Rusty Links in Local Chains},
booktitle = {Proc.\ FTfJP},
publisher = {ACM},
pages = {1--3},
doi = {10.1145/3611096.3611097},
year = {2022},
}
Publisher's Version