Showing 1–7 of 7 results for author: Mosses, P D

Online Name-Based Navigation for Software Meta-languages

Authors: Peter D. Mosses

Abstract: Software language design and implementation often involve specifications written in various esoteric meta-languages. Language workbenches generally include support for precise name-based navigation when browsing language specifications locally, but such support is lacking when browsing the same specifications online in code repositories. This paper presents a technique to support precise name-ba… ▽ More Software language design and implementation often involve specifications written in various esoteric meta-languages. Language workbenches generally include support for precise name-based navigation when browsing language specifications locally, but such support is lacking when browsing the same specifications online in code repositories. This paper presents a technique to support precise name-based navigation of language specifications in online repositories using ordinary web browsers. The idea is to generate hyperlinked twins: websites where verbatim copies of specification text are enhanced with hyperlinks between name references and declarations. By generating hyperlinks directly from the name binding analysis used internally in a language workbench, online navigation in hyperlinked twins is automatically consistent with local navigation. The presented technique has been implemented for the Spoofax language workbench, and used to generate hyperlinked twin websites from various language specifications in Spoofax meta-languages. However, the applicability of the technique is not limited to Spoofax, and developers of other language workbenches could presumably implement similar tooling, to make their language specifications more accessible to those who do not have the workbench installed. △ Less

Submitted 12 September, 2023; originally announced September 2023.

Comments: 6 pages, incl. 5 figures, to be published in Proceedings of the 16th ACM SIGPLAN International Conference on Software Language Engineering (SLE '23), October 23--24, 2023, Cascais, Portugal

Using Spoofax to Support Online Code Navigation

Authors: Peter D. Mosses

Abstract: Spoofax is a language workbench. A Spoofax language specification generally includes name resolution: the analysis of bindings between definitions and references. When browsing code in the specified language using Spoofax, the bindings appear as hyperlinks, supporting precise name-based code navigation. However, Spoofax cannot be used for browsing code in online repositories. This paper is about… ▽ More Spoofax is a language workbench. A Spoofax language specification generally includes name resolution: the analysis of bindings between definitions and references. When browsing code in the specified language using Spoofax, the bindings appear as hyperlinks, supporting precise name-based code navigation. However, Spoofax cannot be used for browsing code in online repositories. This paper is about a toolchain that uses Spoofax to generate hyperlinked twins of code repositories. These generated artefacts support the same precise code navigation as Spoofax, and can be browsed online. The technique has been prototyped on the CBS (Component-Based Semantics) specification language developed by the PLanCompS project, but could be used on any language after specifying its name resolution in Spoofax. △ Less

Submitted 6 March, 2023; originally announced March 2023.

Comments: Accepted for publication in Proc. Eelco Visser Commemorative Symposium (EVCS 2023)

Fundamental Constructs in Programming Languages

Authors: Peter D. Mosses

Abstract: When a new programming language appears, the syntax and intended behaviour of its programs need to be specified. The behaviour of each language construct can be concisely specified by translating it to fundamental constructs (funcons), compositionally. In contrast to the informal explanations commonly found in reference manuals, such formal specifications of translations to funcons can be precise… ▽ More When a new programming language appears, the syntax and intended behaviour of its programs need to be specified. The behaviour of each language construct can be concisely specified by translating it to fundamental constructs (funcons), compositionally. In contrast to the informal explanations commonly found in reference manuals, such formal specifications of translations to funcons can be precise and complete. They are also easy to write and read, and to update when the language evolves. The PLanCompS project has developed a large collection of funcons. Each funcon is defined independently, using a modular variant of structural operational semantics. The definitions are available online, along with tools for generating funcon interpreters from them. This paper introduces and motivates funcons. It illustrates translation of language constructs to funcons, and funcon definition. It also relates funcons to the notation used in some previous language specification frameworks, including monadic semantics and action semantics. △ Less

Submitted 20 August, 2023; v1 submitted 22 July, 2021; originally announced July 2021.

Comments: 26 pages, incl. 3 figures and 7 appendices, accepted for publication in Proceedings of ISoLA 2021; updates the submitted version with clarifications and minor enhancements

ACM Class: D.3.1; F.3.2; D.3.3

A Component-Based Formal Language Workbench

Authors: Peter D. Mosses

Abstract: The CBS framework supports component-based specification of programming languages. It aims to significantly reduce the effort of formal language specification, and thereby encourage language developers to exploit formal semantics more widely. CBS provides an extensive library of reusable language specification components, facilitating co-evolution of languages and their specifications. After int… ▽ More The CBS framework supports component-based specification of programming languages. It aims to significantly reduce the effort of formal language specification, and thereby encourage language developers to exploit formal semantics more widely. CBS provides an extensive library of reusable language specification components, facilitating co-evolution of languages and their specifications. After introducing CBS and its formal definition, this short paper reports work in progress on generating an IDE for CBS from the definition. It also considers the possibility of supporting component-based language specification in other formal language workbenches. △ Less

Submitted 23 December, 2019; originally announced December 2019.

Comments: In Proceedings F-IDE 2019, arXiv:1912.09611

ACM Class: D.3.1; D.2.6; D.2.13; F.3.2

Journal ref: EPTCS 310, 2019, pp. 29-34

A Modular Structural Operational Semantics for Delimited Continuations

Authors: Neil Sculthorpe, Paolo Torrini, Peter D. Mosses

Abstract: It has been an open question as to whether the Modular Structural Operational Semantics framework can express the dynamic semantics of call/cc. This paper shows that it can, and furthermore, demonstrates that it can express the more general delimited control operators control and shift. It has been an open question as to whether the Modular Structural Operational Semantics framework can express the dynamic semantics of call/cc. This paper shows that it can, and furthermore, demonstrates that it can express the more general delimited control operators control and shift. △ Less

Submitted 20 June, 2016; originally announced June 2016.

Comments: In Proceedings WoC 2015, arXiv:1606.05839

ACM Class: D.3.3; F.3.2

Journal ref: EPTCS 212, 2016, pp. 63-80

Flag-Based Big-Step Semantics

Authors: Casper Bach Poulsen, Peter D. Mosses

Abstract: Structural operational semantic specifications come in different styles: small-step and big-step. A problem with the big-step style is that specifying divergence and abrupt termination gives rise to annoying duplication. We present a novel approach to representing divergence and abrupt termination in big-step semantics using status flags. This avoids the duplication problem, and uses fewer rules a… ▽ More Structural operational semantic specifications come in different styles: small-step and big-step. A problem with the big-step style is that specifying divergence and abrupt termination gives rise to annoying duplication. We present a novel approach to representing divergence and abrupt termination in big-step semantics using status flags. This avoids the duplication problem, and uses fewer rules and premises for representing divergence than previous approaches in the literature. △ Less

Submitted 10 May, 2016; originally announced May 2016.

Comments: To appear in The Journal of Logical and Algebraic Methods in Programming, Special Issue: 26th Nordic Workshop for Programming Theory, 2014

Robustness of Equations Under Operational Extensions

Authors: Peter D. Mosses, MohammadReza Mousavi, Michel A. Reniers

Abstract: Sound behavioral equations on open terms may become unsound after conservative extensions of the underlying operational semantics. Providing criteria under which such equations are preserved is extremely useful; in particular, it can avoid the need to repeat proofs when extending the specified language. This paper investigates preservation of sound equations for several notions of bisimilarity o… ▽ More Sound behavioral equations on open terms may become unsound after conservative extensions of the underlying operational semantics. Providing criteria under which such equations are preserved is extremely useful; in particular, it can avoid the need to repeat proofs when extending the specified language. This paper investigates preservation of sound equations for several notions of bisimilarity on open terms: closed-instance (ci-)bisimilarity and formal-hypothesis (fh-)bisimilarity, both due to Robert de Simone, and hypothesis-preserving (hp-)bisimilarity, due to Arend Rensink. For both fh-bisimilarity and hp-bisimilarity, we prove that arbitrary sound equations on open terms are preserved by all disjoint extensions which do not add labels. We also define slight variations of fh- and hp-bisimilarity such that all sound equations are preserved by arbitrary disjoint extensions. Finally, we give two sets of syntactic criteria (on equations, resp. operational extensions) and prove each of them to be sufficient for preserving ci-bisimilarity. △ Less

Submitted 29 November, 2010; originally announced November 2010.

Comments: In Proceedings EXPRESS'10, arXiv:1011.6012

ACM Class: F.3.2; D.3.1; D.2.1

Journal ref: EPTCS 41, 2010, pp. 106-120