Formal Semantics by a Combination of Denotational Semantics and High-Level Petri Nets

Abstract

Denotational semantics has proved to be an excellent tool for the specification of nearly all kinds of declarations and commands in sequential languages, but the description of concurrent processes is in practice nearly impossible.

High-level Petri nets, on the other hand, have proved their value in the specification of communication and synchronization of concurrent processes.

We propose to combine the two models into a single approach, where denotational semantics is used to build up environments and to describe store transformations, while Petri nets are used to describe sequencing and communication.