Defect Report Concerning ISO International Standard 8807 and Proposal for a Correct Flatenning of LOTOS Parametrized Types.

Hubert Garavel and Mihaela Sighireanu

Rapport SPECTRE, 95-11, VERIMAG, Grenoble, July 1995

Abstract:

We report a defect in the definition of LOTOS (ISO/IEC standard IS-8807). We show that the standard semantics for parameterized and actualized types - although it is consistent in itself - is not satisfactory in case of multiple instantiations of the same generic type, and leads to strange behaviours in existing LOTOS tools. We indicate how to avoid this problem when writing formal specifications in LOTOS, and we also propose a modification of the flattening mechanism defined in IS-8807 in order to solve this problem.

9 pages

PDF

PostScript