Operational Semantics of DEMOS 2000

Tofts, Chris ; Birtwistle, Graham

HP Development Company

关键词: semantics;    discrete event simulation;    functional programming;    correctness;   

RP-ID  :  HPL-2001-263

学科分类：计算机科学（综合）

美国|英语

来源: HP Labs

【 摘 要 】

We take a process oriented simulation language, DEMOS 2000, and define its operational semantics. This achieves two goals: firstly, we can unambiguously define the behaviour of any DEMOS program; secondly, we can use the semantics to check the behaviour of any implementation of the language. An operational semantics has been given for the simple synchronisation fragment of mu DEMOS before (Birtwistle & Tofts, 1993, 1994), but that fragment lacked many features of a complete discrete event simulation language. DEMOS 2000 is a slight redesign of DEMOS that frees it from the underlying Simula. In this semantics we give an account of the complete language which includes features such as: parametric classes; value, resource, entity handling synchronisations; multi-way competing synchronisations; priority; conditional synchronisations; random number sampling; data dependent entities; data dependent work. Notes: Graham Birtwistle, School of Computer Studies, Leeds University, Woodhouse Lane, Leeds, UK. 46 Pages