A Comparison of the Declarative Modelling Languages B, Dash, and TLA+

Declarative behavioural modelling is a powerful modelling paradigm that enables users to model system functionality abstractly and concisely. We compare two well-used formal declarative modelling languages, B and TLA+, with a new modelling language called Dash. Dash is an extension of Alloy with explicit syntactic constructs for modelling...More