Mechanizing the Denotational Semantics of the Clock Constraint Specification Language

2018 ◽  
pp. 385-400
Author(s):  
Mathieu Montin ◽  
Marc Pantel
Keyword(s):  
Denotational Semantics ◽  
Specification Language ◽  
Constraint Specification ◽  
Clock Constraint Specification Language

The clock constraint specification language for building timed causality models

2009 ◽  
Vol 6 (1-2) ◽  
pp. 99-106 ◽  
Author(s):  
Frédéric Mallet ◽  
Julien DeAntoni ◽  
Charles André ◽  
Robert de Simone
Keyword(s):  
Specification Language ◽  
Constraint Specification ◽  
Clock Constraint Specification Language

A Model-Based Concurrent Specification Language over CML: Semantic Foundations

1997 ◽  
Vol 07 (03) ◽  
pp. 329-356
Author(s):  
Maurad Debbabi
Keyword(s):  
Wide Spectrum ◽  
Denotational Semantics ◽  
Specification Language ◽  
Return Of Results ◽  
Static Semantics ◽  
Model Based ◽  
Communication Effects ◽  
Definition Of ◽  
Theoretical Foundations ◽  
Spectrum Model

In this paper we address the problem of specification and design of concurrent systems. More accurately, we present the definition of a new specification language that is formal, wide-spectrum, model-based, concurrent, polymorphic and strongly implicitly typed. The language is built upon a concurrent, funtional and imperative programming language: Concurrent ML. Specification aspects are supported thanks to the addition of some specification constructs and also by allowing axioms to ML structures and signatures. The resulting specification language is thus highly expressive though it embodies a restricted number of concepts. We present here the motivations underlying the definition of such a language as well as the design choices. Furthermore, we introduce the specification and development methology and illustrate it on various examples. We will see that many specification styles are allowed: algebraic, applicative, state-based, concurrent applicative and concurrent imperative. We show that the language rests on secure theoretical foundations exemplified by formal syntactic and semantic definitions. The latter consists in a static semantics together with a dynamic semantics. The static semantics reconstructs not only principal types but also minimal side and communication effects. This is done thanks to an extension of the type and effect discipline. The language is also endowed with a dynamic denotational semantics. The underlying model is based on an extension of the acceptance trees model to handle value-passing, communication, assignment, sequencing, return of results and higher order objects.

Sign in / Sign up

Export Citation Format

Share Document