The DisCo Home Page

The Language Reference manual of DisCo

Table of Contents

Introduction
1 Basic definitions
1.1 Notes about the syntax
1.2 Comments
1.3 Identifiers and literals
1.4 Reserved words
1.5 Types and parameter lists
2 System part
2.1 Importing
2.2 Renaming
2.3 Combining actions
2.4 System body
2.5 Export list
3 Classes
3.1 Class body
3.2 States
3.3 Variable definitions
3.4 Extension
3.5 Inheritance
3.6 Assertions and initial conditions
4 Actions
4.1 Action body
4.2 Assignment statement
4.3 State transitions
4.4 Conditional statement
4.5 Local assertions
4.6 Derived actions
5 Stuff types
6 Functions
6.1 Function body
7 Global assertions
8 Creation
8.1 Assignment
8.2 Object creation
8.3 For statement
8.4 Procedure definition and procedure call
9 Expressions
9.1 Primaries
9.2 Operators and priorities
9.3 Syntax of expressions
9.4 Evaluation order and nonexistent components
10 Naming rules
10.1 Uniqueness of names
10.2 The structure of names
11 Multiple imports
11.1 Classes, functions and assertions in a union
11.2 Actions in a union

Introduction

This document is a reference manual of DisCo, and it assumes some familiarity with the underlying ideas of the language. Examples in this manual are mainly of a syntactic nature, and the reader should consult other material to learn about the intent of the constructs.

The basic entities of DisCo are objects and actions. Actions are the atomic units of execution. An object can be characterized as a data structure together with the capability to participate in certain actions.

An action has a guard, optional parameters, a collection of roles, i.e., formal participants, and a body. It is enabled and (its body) can be executed for some assignment of parameter values and actual participating objects, when the guard is true for this assignment. When several actions are enabled, or one is enabled for several choices of parameter values and participants, the selection is nondeterministic.

The global state of execution is totally determined by the local states of the objects. The local state of an object is partitioned into components called the discrete state (henceforth also called the state, for short), and data components. A data component is either constant or variable.

The alternatives for the (discrete) state of an object form a statechart-like hierarchical structure with the possibility for both nested and parallel states. Each data component is associated with some state in this structure. A state therefore provides a scope in which its constants, variables, and substates are available.

The local state of an object can be modified only when executing an action in which the object participates. A transition of the discrete state is expressed by a special state transition statement. If constants are associated with the state(s) entered, their values are then provided as actual parameters. A constant remains unchanged as long as the associated state is preserved. Assignment statements are available for the variables of the current states.

Each object belongs to a class of similar objects. A mechanism for class inheritance provides the possibility for nested objects.

A DisCo program consists of two separately given parts called the system part and the creation. All classes and actions are given in the system part. The creation part creates and initializes the world of objects in which the actions are to be executed. Each creation part is therefore bound to a specific system part, but not vice versa.

Motivation of some language properties

Superposition is a design method where new detail is added to a system stepwise. Technically, the system is imported in DisCo into a new system where the modifications are made. These modifications include extension of previously introduced objects (classes) with new components, refinement of previously given actions to deal with the new state components, and introduction of new objects (classes) and actions. Computations of an imported system can also be restricted by strengthening the guards of actions. All safety properties of imported systems are preserved in pure superposition, but liveness properties may be violated (because of guard strengthening, for instance).

A special way to extend system state is inheritance. Inheriting a class of an imported system into (some state of) another class leads to subobject hierarchy where the inherited parts act as (sub)objects in their own right and can therefore participate in actions defined for their classes. Actions that concern such subobjects can, however, be specialized to take the specific context of inheritance into consideration. If inheritance takes place to the outermost state of a class only, the situation is similar to superposition, and all safety properties of imported systems are preserved. Otherwise, a subobject may become inactive by the enclosing object exiting the associated state, in which case the relationship between the two systems is more complex.

DisCo specifications are intended to describe reactive systems together with their environments. Interaction between a system and its environment takes place through an interface. Specifications can therefore start with an interface description, which is given as a system in its own right, with separate sets of actions for the system and the environment. Both the system and the environment can then be derived of this interface system by independent steps of superposition refining system actions and environment actions, respectively. It is also possible for a system to have several interfaces. An intermediate level in the OSI model of data communications, for instance, has two interfaces, one for each direction in the hierarchy.

Modules in DisCo are systems that provide a mechanism to restrict their modification and the visibility of their contents. When a module is imported, actions and classes in the module are not refineable, unless imported by an export list. A module may have several named export lists, by which access is obtained to different units in the module.

An export list may include one or more stuff types. A stuff type is a type whose structure and contents are irrelevant to the module where it is introduced. When a module is imported by an export list that contains a stuff type, the stuff type can be refined to a record structure. Several parallel refinements of the same stuff type may also coexist.

System invariants can be expressed by assertions, which are either global or local conditions that should always hold. When a DisCo system is executed, these assertions are checked, and the execution is aborted, if any assertion is violated. Conditions that must hold immediately after the creation phase can be given as initial conditions. States may also have local initial conditions that are checked whenever the states are entered.

The creation part creates a world of objects. The created world has to fulfill all assertions and initial conditions given in the system part. The creation part consists of traditional sequential program statements and procedures.

1 Basic definitions

1.1 Notes about the syntax

(0.1)  nonterminal =


syntactic_definition

Nonterminals may be prefixed with semantic information in italics. Braces ({}) indicate repetition of zero or more times, brackets ([]) denote an optional part, and a bar (|) separates syntactic alternatives. Brackets and bars in single quotes (e.g. '|') are part of the language. Words in boldface are reserved words of the language.

2.4.1) begin with a reserved word and an identifier. They end with the reserved word end, optionally followed by the identifier.

1.2 Comments

1.2.1

The language allows comments in the end of any lines. A comment begins with a double hyphen (--) and ends at the end of the line.

1.3 Identifiers and literals

1.3.1

An identifier is a sequence of letters, digits, and underscores. The first character shall be a letter, the last one shall not be an underscore, and two consecutive underscores are not permitted.

(1.1)  identifier =

letter {[ _ ] letter_or_digit }

(1.2)  letter_or_digit =

letter | digit

1.3.2

A letter is a letter between a and z. Upper and lower case letters are considered equal except in strings.

1.3.3

Numbers are sequences of decimal digits.

(1.3)  number =

digit { digit }

1.3.4

Entities are referenced in the language by names that are either single identifiers or are prefixed by other names. The rules for using prefixed names will be given in (10.1)-(10.3).

(1.4)  simple_name =

identifier

(1.5)  name =

{ identifier . } simple_name

(1.6)  simple_name_list =

simple_name { , simple_name }

(1.7)  name_list =

name { , name }

Example 1.3 Identifiers

124
23455646
Variable
Quite_a_long_one_combined_with_a_number_1

32_3
Ending_in_underscore_
2wrong
No_specials_#
No__double_underscores

1.4 Reserved words

1.4.1

The following words are reserved:

1.4.2

Reserved words shall not be used as identifiers.

1.5 Types and parameter lists

1.5.1

There are two predefined types, integer and boolean. The name of a class denotes an object type. The values of an object type are references to objects of the given type. A set type stands for collections, and a sequence type for sequences of objects or values of the given type. A stuff type is a type whose contents are not defined when the type is introduced. Stuff types are introduced by export lists, see 2.5.1. In the syntax rules, type_simple_name refers to any of these types.

(1.8)  type =

type_simple_name | set type_simple_name 
| sequence type_simple_name

1.5.2

Some language constructs involve lists of formals that are to be associated with values of given types.

(1.9)  formals_list =

formals { ; formals }

(1.10)  formals = formals_name_list : type { , subobject_condition }

(1.11)  formals_name_list =

[ * ] formal_simple_name { , [ * ] formal_simple_name }

(1.12)  subobject_condition =

subobject_simple_name = object_component_name

(1.13)  formals_with_defaults_list =

formals_with_defaults { ; formals_with_defaults }

(1.14)  formals_with_defaults = formals_name_list [ : type [ := expression ] ]

1.5.3

Depending on context there may be restrictions on the types that can be used for formals. The context also tells, whether actual values are assigned to formals by nondeterministic selection or by an explicit list of actuals.

1.5.4

An asterisk (*) before a formal simple name can only be used in participant lists of actions, in order to indicate fairness requirements, see 4.0.5. Type of a formal participant can be left out only, if fairness requirements are added by an action derivation (see 4.6.5).

1.5.5

Subobject conditions can be used only within participant lists in action refinement or specialization (see 4.6.6).

1.5.6

Actual parameters are associated with formal parameters either by position or by formal names. The two methods can be mixed, but all positional associations shall precede the named associations.

(1.15)  actuals_list =

formal_simple_name := expression 
{ , formal_simple_name_list := expression }

| expression [ , actuals_list ]

Example 1.5 Types, formals and actuals lists

function example (first, second: integer; third: boolean) return integer is

a.b := example (2, 4, false);

state a, b (first: integer; second: integer := 3; third: boolean := true);

→ b(4,5);
→ b(2, third := false);

2 System part

2.0.1

The system part of a DisCo program defines a set of classes and actions, together with optional functions, global assertions, and global initial conditions. Its general structure is the following:

(2.1)  system =

system_or_module simple_name

[ import_part ] is

    system_body

end [ simple_name ] ;

(2.2)  system_or_module = system | module

(2.3)  import_part =

import_clause  rename_list  use_list  combine_list

(2.4)  rename_list =

{ rename_declaration }

(2.5)  use_list =

{ use_statement }

(2.6)  combine_list =

{ combination }

2.0.2

Use statement is discussed in Section 5 (Stuff types).

2.1 Importing

2.1.1

A system may utilize other systems by importing them.

(2.7)  import_clause =

import imported_system_list ;

(2.8)  imported_system_list = imported_system { , imported_system }

(2.9)  imported_system =

system_or_module_simple_name [ ( export_simple_name_list ) ]

2.1.2

The difference between a system and a module is in the visibility and modifiability of actions and classes. When importing a system, all its units are visible and accessible for the importer. When a module is imported, only the actions and classes of the specified export lists are refineable. If an action is not in any of these export lists, it is not even visible. A class or stuff type that is not in the export lists is visible and may be used as a type of a variable or parameter. The names of export lists shall be given when a module is imported.

2.1.3

If the imported systems are independent (see 11.0.2), all their units become units of the importing system, and can then be transformed in it. In the general case, imported systems may share a common imported system or module. A union of the imported systems is then formed as described in Section 11, and this union is the basis for the transformations to be given in the importing system.

Example 2.1 Importing

module M import S is

system S import M(exporting) is

2.2 Renaming

2.2.1

Renaming is used to maintain uniqueness of identifiers. Every visible unit of a system shall have a single unique name. Only imported units can be renamed.

(2.10)  rename_declaration =

rename renaming { , renaming } ;

(2.11)  renaming =

old_name as new_simple_name

2.2.2

When renaming, the old name shall be prefixed by the name of the system in question.

2.3 Combining actions

2.3.1

Under certain circumstances the union of imported systems contains actions that are obtained by combining actions of the different imported systems. The combine list is associated with this, and its meaning will be explained in 11.2.10 and 11.2.11.

(2.12)  combination =

combined simple_name of action_name_list ;

2.3.2

Action names in the name list shall be prefixed by the system names in question.

2.4 System body

2.4.1

The system body contains definitions of units: classes, actions, functions, global assertions, and global initial conditions.

(2.13)  system_body =

export_list  class_list  function_list  initially_list  assertion_list  action_list

(2.14)  export_list =

{ export }

(2.15)  class_list =

{ class }

(2.16)  function_list =

{ function_definition }

(2.17)  initially_list =

{ global_intitial_condition }

(2.18)  assertion_list =

{ global_assertion }

(2.19)  action_list =

{ action }

2.4.2

The lists of a system body can also be empty.

2.4.3

Classes are discussed in Section 3 (Classes), functions in Section 6 (Functions) on, global initial conditions and global assertions in Section 7 (Global assertions), and actions in Section 4 (Actions).

2.5 Export list

2.5.1

An export list groups together a set of actions and classes. For instance, one export list may introduce environment actions and classes, and another may introduce internal actions and classes. Each group can then be refined separately. When stuff types are introduced in an export list, the actions of the export list can distinguish between different refinements of the stuff types. For the meaning and use of stuff types, see Section 5.

(2.20)  export =

export export_simple_name is

    [ stuff stuff_type_simple_name_list ; ]

    [ class class_simple_name_list ; ]

    [ action action_simple_name_list ; ]

end [ export_simple_name ] ;

2.5.2

Stuff, action, and class lists in export lists shall be disjoint; a stuff type, action, or class can be a member of only one export list.

2.5.3

Export lists can be defined for modules only.

Example 2.5 Export list

export implementation is

  class in_data, out_data;

  action use_in_data, produce_out_data;

end;

export specification is

  stuff data;

  action produce_data, consume_data;

end;

3 Classes

3.0.1

New classes can be defined, and imported classes can be extended in a system part.

(3.1)  class =

class_definition | class_extension

(3.2)  class_definition =

class simple_name [ ( formals_with_defaults_list ) ] is

    class_body

end [ simple_name ] ;

3.0.2

The optional parameters of a class, i.e., constants of its outermost scope, are given in the heading of the class definition. Values of their parameters are set during object creation, or, in the case of nested objects, in class inheritance or state transitions.

3.1 Class body

3.1.1

A class body consists of state definitions, variable definitions, state extensions, class inheritances, local assertions, and initial conditions.

(3.3)  class_body =

{ class_component }

(3.4)  class_component =

state_definition | variable_definition | state_extension | inheritance 
| local_assertion | local_initial_condition

Example 3.1 Classes

The following is a complete class definition with one data component, two state definitions, an extension of one state, and an assertion:

class lift is

  at_floor: floor;

  state *up, down;

  state *stopped, moving;

  extend stopped by

    state *door_closed, door_open;

  end stopped;

  assert at_floor <> null;

end lift;

3.2 States

3.2.1

States are introduced by state definition statements.

(3.5)  state_definition =

state state_item { , state_item } ;

(3.6)  state_item =

[ hide ] [*] simple_name [ ( formals_with_defaults_list ) ]

3.2.2

If there are several state definition statements within the same immediate scope, these correspond to state components that are parallel in the sense that the set of possible states is the Cartesian product of these definitions.

3.2.3

When given in a state extension, a state definition introduces substates of the state being extended.

3.2.4

Classes and states are closely related in the sense that a class name can be understood as the outermost state in the state hierarchy of an object. (The class body is then an extension of this outermost state.) A class and all its substates create scopes of their own.

3.2.5

When an object is in a given state, this state is said to be active. Otherwise the state is inactive. Inherited subobjects may become inactive, if the inheriting scope becomes inactive. Derivations of imported actions may not inactivate or activate subobjects (see 4.6.4). If an object is not an inherited subobject, it is always active.

3.2.6

A state may be specified as hidden. In a hidden state an object is disabled from participating in imported actions. For new actions introduced in the current system or in systems importing the current system the hide clause has no effect. The hierarchical state structure allows an object to be in several hidden states at the same time.

3.2.7

Prefixing a state name with a asterisk (*) indicates a default state. There shall be exactly one default state in each state definition, and this shall not have any parameters without default values.

3.2.8

State parameters are similar to class parameters, except that their values are set in state transition statements.

Example 3.2 States

state a, b (count: integer), *c, d (reference: another_class);

3.3 Variable definitions

3.3.1

A variable definition given in the immediate scope of a class or state associates a variable with this scope.

(3.7)  variable_definition =

simple_name_list : type [ := expression ] ;

3.3.2

The optional expression is a default value expression that is evaluated when the associated scope is entered, i.e., an object is created or a state is entered. If the default expression is omitted, type integer is assumed value 0 (zero), boolean false, reference null, set ∅, and sequence <>, respectively.

3.3.3

The data components referenced in a default expression must have been defined earlier, either in the current scope or in an enclosing scope of the same class. Indirect references through object valued components are not allowed.

3.3.4

Variable definitions are also available for defining local variables in the creation part.

3.4 Extension

3.4.1

Extension allows the introduction of an immediate substate structure to a class or state. Within a class body only the states of this class can be extended, and a state can be extended only once.

(3.8)  extension =

extend state_or_imported_class_name 
[ ( ... formals_with_defaults_list ) ] by

    class_body

end [ name ] ;

3.4.2

Extension of the top level of a class is allowed for imported classes only. Classes imported from a module shall not be extended unless they are members of an imported export list.

3.4.3

New parameters of classes and states shall have default values.

3.4.4

When extending an imported class, the result is equivalent to a class where the new definitions are added to the old ones. The non-extended version of the class is then no more available.

3.4.5

States belonging to inherited parts (see 3.5.1) can be extended only by extending the inherited class.

3.4.6

For the effects of combining parallel extensions in separate systems, see Section 11.1.

Example 3.4 Class extension

class lift is

  at_floor: floor;

  assert at_floor <> null;

end lift;

extend lift by

  state *up, down;

end lift;

extend lift by

  state *stopped, moving;

  extend stopped by

    state *door_closed, door_open;

  end stopped;

end lift;

class lift is

  at_floor: floor;

  state *up, down;

  state *stopped, moving;

  extend stopped by

    state *door_closed, door_open;

  end stopped;

  assert at_floor <> null;

end lift;

Figure 1 A statechart for class lift

3.5 Inheritance

3.5.1

An inherit statement allows the creation of nested objects.

(3.9)  inheritance =

inherit class_simple_name [ ( actuals_list ) ] [ as simple_name ] ;

3.5.2

An inherited class must have been defined in an imported system.

3.5.3

For the inheriting class the effect is similar to a state definition statement that introduces a single auxiliary state, together with its extension that corresponds to the inherited class body. Recursive inheritance is not permitted, which means that the state structure of all objects is finite.

3.5.4

The as part renames an inherited part inside the inheriting class. This is required if the same class is inherited more than once in the same scope.

3.5.5

Within an object of the inheriting class, the inherited part is an object in its own right. When the former is in the state that involves the inherited part, the latter is also active. (This is always the case when inheritance takes place in the outermost scope of the inheriting class.) Otherwise it is inactive. Only active objects can participate in actions. An inactive object has no current state or data components, but it has a unique reference. Therefore, it can appear in values involving references.

3.5.6

If an inherited class has parameters without default values, these shall be bound in the inherit statement to default expressions. Default values given by class definition or extension can be overridden here.

3.6 Assertions and initial conditions

3.6.1

Class definitions may contain local assertions and initial conditions that express integrity constraints within single objects.

(3.10)  local_assertion =

assert boolean_expression ;

(3.11)  local_initial_condition =

initially boolean_expression ;

3.6.2

An assertion shall be invariantly true, except in the middle of executing an action. An initial condition associated with a state (or class) shall be true for an object of this class whenever this state (or class) becomes active. If an assertion or initial condition does not hold, a run-time error is generated.

3.6.3

A local assertion or initial condition within a class definition can only refer to the local state of a single object of the current class.

3.6.4

Assertions and initial conditions cannot have side effects.

4 Actions

4.0.1

Actions are the units of execution where all state changes take place. An action has parameters, participants, a guard, and a body.

(4.1)  action =

action_definition | action_transformation

(4.2)  action_definition =

action simple_name [ ( formals_list ) ] by formals_list is

when boolean_expression do

    [ body ]

end [ simple_name ] ;

4.0.2

The optional parameters of an action are specified in the first list of formals, and their types are restricted to predefined and stuff types. Actual values are assigned to parameters when an action is activated for execution. This assignment is nondeterministic and is restricted only by the guard.

4.0.3

The second list of formals specifies the participants. This list shall be nonempty, and the types are restricted to object types. Similarly to action parameters, the assignment of actual participants is nondeterministic, and is restricted only by the guard.

4.0.4

Each formal participant represents a role. When an action is executed, an object is assigned to each role. The same object cannot be assigned to more than one role at the same time. In addition, an object and its subobject cannot be assigned to different roles at the same time, except when a subobject condition explicitly specifies this to be the case (see 4.6.6).

4.0.5

Prefixing a participant name by an asterisk indicates the following fairness requirement. If an action is infinitely often enabled so that the same object could participate in the same prefixed role, then the action has to be executed infinitely often with this object in the prefixed role. If fairness is required for more than one participant, the fairness condition above is required for each combination of such participants. (Since an implementation deals with finite executions only, this has no effect on the DisCo environment.)

4.0.6

The boolean expression is the action guard. A guard can refer to the parameters and the participants of the action. It may also involve quantified expressions, references to object components via object references, and function calls that involve any of these or closures.

4.0.7

An action can be executed only if its guard is true for the selected parameter values and actual participants. Note: A guard of an imported action may be implicitly strengthened by hidden states that are added to the participants.

4.1 Action body

4.1.1

An action body consists of four kinds of statements: assignments, conditional statements, state transitions, and local assertions.

(4.3)  body =

statement { statement }

(4.4)  statement =

multiple_assignment | multiple_state_transition | conditional_statement 
| local_assertion

4.1.2

Statements of an action body can only refer to the participants and parameters of the action. Indirect reference to the local state of an object is not allowed via object valued data components.

4.1.3

If a participant of an action belongs to an imported class (see 2.1), the body is not allowed to modify any of the imported states or data components. The body can only modify components that have been added in the current system by extension.

Example 4.1 Actions

action move_and_stop by li: lift; fl: floor is

when (li.at_floor.upper = fl & li.up | li.at_floor.lower = fl & li.down) & li.moving do

  li.at_floor := fl;

  → li.stopped;

end move_and_stop;

4.2 Assignment statement

4.2.1

A single assignment assigns the value of an expression to a variable. A multiple assignment is expressed using a double bar (||) as a delimiter. All right-hand sides of a multiple assignment are evaluated before any of the assignments takes place. Multiple assignment to the same variable is not allowed in one statement.

(4.5)  multiple_assignment =

assignment { || assignment } ;

(4.6)  assignment =

variable_name := expression

4.3 State transitions

4.3.1

A multiple state transition changes the discrete states of one or more of the participating objects. If the states to be entered need parameters, these must be given in this connection.

(4.7)  multiple_state_transition =

state_transition { || state_transition } ;

(4.8)  state_transition =

transition_symbol

     state_name [ ( actuals_list ) ] 

      { . state_simple_name [ ( actuals_list ) ] }

(4.9)  transition_symbol = → | ->

4.3.2

The destination state of each transition shall be uniquely determined by the sequence of nested states given and by the default states of the class.

4.3.3

Multiple state transitions are executed in parallel. In the case of parallel states, a state transition statement may contain several transitions for the same object.

4.3.4

A transition is uniquely determined by its source and destination states, and by the rule that no state in the hierarchy is both exited and entered in a single transition.

4.3.5

If several nested states with parameters are entered, each of them must be explicitly given in the transition, and the actual parameters must follow the corresponding state names.

4.3.6

A transition to an active state is considered a null transition. In this case, the values of actual parameters can be omitted. If they are present, they have to agree with the old values of the parameters. This is checked by an implicit assertion.

4.4 Conditional statement

4.4.1

Conditional execution of statements is expressed by a conventional conditional statement. The alternatives of the conditional statement have the same structure as an action body, or a creation statement list in a creation part (see 8.0.3).

(4.10)  conditional_statement =

if boolean_expression then

    if_alternative

{ elsif boolean_expression then

    if_alternative }

[ else

    if_alternative ]

end if;

(4.11)  if_alternative =

body | creation_statement_list

4.5 Local assertions

4.5.1

An action body may include local assertions, see 3.6.

4.5.2

A local assertion within an action body shall be true when checked at the place of its occurrence. If it is not true, a run-time error is generated.

4.5.3

Similarly to other statements in an action body, local assertions can only reference the parameters and participants of the action.

4.5.4

Assertions cannot have side effects.

Example 4.5 Local assertion

refined rec_message is

when ... do

  assert qi.candidate = mc.data;

  ...

  → qi.idle;

end;

4.6 Derived actions

4.6.1

Imported actions can be used as a basis for derived actions. Derivation takes place either by explicit transformations (i.e., refinements and specializations described in this section), or implicitly by hidden states (see 3.2.6, and 4.0.7) or by composition of derived actions (see section 11). Derivation may add new parameters and participants, introduce new fairness requirements, strengthen the guard, and add new statements to be executed immediately before and after the old body. If no explicit or implicit derivations are applied to an imported action, it is taken as such and is called an identity derivation of the old action.

(4.12)  action_transformation =


refined_or_specialized action_simple_name [ ( ... formals_list ) ] 
[ of base_action_simple_name ]

[ by ... formals_list ] is

when [ ... ] [ boolean_expression ] do

    [ body ]

    ...

    [ body ]

end [ simple_name ] ;

(4.13)  refined_or_specialized = refined | specialized

4.6.2

An ellipsis (...) refers to a part taken from the imported action. If it is omitted in the guard, the old guard is replaced by the new one; otherwise the new guard is added as another conjunct to the old one.

4.6.3

If the old guard is replaced by a new one, the new one is assumed to imply the old one, and a corresponding assertion is implicitly generated.

4.6.4

The new parts of a body shall not modify imported components of any participants (see also 4.1.3). Furthermore, derived actions shall not inactivate or activate inherited subobjects (see also 3.2.5).

4.6.5

Fairness requirements (see 4.0.5 ) can be introduced for an old participant by prefixing the participant's name by an asterisk. The type of a formal participant is omitted in this case.

4.6.6

A subobject condition in a formal participant list specifies an old participant to be a subobject of a new participant. In this case, an object and its subobject have separate roles in the action. See also 4.0.4.

4.6.7

When the construct refined B of A is used, an action A is refined, the result is named B, and A is removed. Several refinements may be given in the same system for the same action, causing multiple refined versions of the original action to appear. The phrase refined A is synonymous to refined A of A.

4.6.8

Each specialization of an action introduces a derived action exactly as in the case of refinement. In addition, the old action remains in a form that is implicitly derived by strengthening the old guard as follows. If any specialization of the action has a subobject condition for some role, then an object that is such a subobject cannot be assigned to the corresponding role in this implicitly derived action.

4.6.9

Every specialized action shall be given a new name.

4.6.10

An action shall not be both refined and specialized in the same system.

4.6.11

For composition of parallel derivations imported from separate systems, see Section 11.2.

Example 4.6 Action refinement

action move by li: lift; fl: floor is

when li.at_floor.upper = fl | li.at_floor.lower = fl do

  li.at_floor := fl;

end move;

refined move is

when li.at_floor.upper = fl & li.up | li.at_floor.lower = fl & li.down do

  ...

end move;

action change_direction by li: lift; fl: floor is

when li.at_floor = fl do

  if li.down & fl.upper <> null then

    → li.up;

  elsif li.up & fl.lower <> null then

    → li.down;

  end if;

end change_direction;

refined move_and_pass of move is

when ... li.moving & (li.up & fl.upper <> null | li.down & fl.lower <> null) do

  ...

end move_and_pass;
refined move_and_stop of move is

when ... li.moving do

  ...

  → li.stopped;

end move_and_stop;

action move_and_pass by li: lift; fl: floor is

when (li.at_floor.upper = fl & li.up | li.at_floor.lower = fl & li.down)

  & (li.moving & (li.up & fl.upper <> null | li.down & fl.lower <> null) do

  li.at_floor := fl;

end move_and_pass;

action move_and_stop by li: lift; fl: floor is

when (li.at_floor.upper = fl & li.up | li.at_floor.lower = fl & li.down) & li.moving do

  li.at_floor := fl;

  → li.stopped;

end move_and_stop;

5 Stuff types

5.0.1

A stuff type represents a block of data whose contents are insignificant in the module where it is introduced. Stuff types are introduced in module export lists, see 2.5.1.

5.0.2

A stuff type can be used like any other type (as a type of a parameter or component) in the scope of its definition, and when the export list it belongs to is not imported, see also 2.1.2. Once a stuff type is refined, an object component of the type can not be referred to. However, action parameters can be referred; for explanation see 5.0.4. There are no operators defined for a stuff type.

5.0.3

Each stuff type has an implicit tag field. A use statement determines a unique value for this tag, together with an associated refinement of the stuff type as a record structure. The record is defined by a formals list that introduces the names and types of the components, which can then be referenced like any other state components. A stuff type may be refined to contain components of other stuff types, but recursion is not allowed either directly or indirectly. All stuff types of an imported export list shall be refined by a use statement.

(5.1)  use_statement =

use stuff_refinement_list rename_declaration

(5.2)  stuff_refinement_list =

stuff_refinement { , stuff_refinement }

(5.3)  stuff_refinement = stuff_name ( formals_list )

5.0.4

A use statement duplicates (specializes) all actions of an export list. In this specialization the guards are implicitly strengthened so that for each action parameter of this stuff type a test is added that the tag has the value associated with the use statement. Action specializations created by a use statement have to be renamed to avoid confusion with the original versions and with other specializations of the same actions. The original versions of these actions are not removed, but their guards are implicitly strengthened to be false when the tag is the one associated with the use statement. The specialized actions can be refined or specialized further in the same system.

5.0.5

The same stuff type may have several different refinements with associated specialized actions. Actions that access the stuff type but are not in the export list cannot distinguish between the different refinements.

Example 5.0 Stuff types

A message is first put into a queue of an object of the class sender. Then it is moved to a communication channel (class channel) by action send, from which it is taken by receive and put into another queue (class receiver). The modelled communication channel is a reliable point to point channel.

module Mid_Level_Interface is

  export up is

    stuff message;

    action enqueue, dequeue;

  end;

  export down is

    class channel, receiver, sender;

    action send, receive;

  end;

  class channel is

    state *idle, busy (data: message);

  end;

  class sender (ch: channel) is

    queue: sequence message := <>;

  end;

  class receiver (ch: channel) is

    queue: sequence message := <>;

  end;

  action enqueue (ms: message) by s: sender is

  when true do

    s.queue := s.queue & <ms>;

  end;

  action dequeue (ms: message) by r: receiver is

  when size (r.queue) > 0 & ms = head (r.queue) do

    r.queue := tail (r.queue);

  end;

  action send by s: sender; ch: channel is

  when s.ch = ch & size (s.queue) > 0 & ch.idle do

    → ch.busy (head (s.queue));

    s.queue := tail (s.queue);

  end;

  action receive (ms: message) by r: receiver; ch: channel is

  when r.ch = ch & ms = ch.busy.data do

    r.queue := r.queue & <ms>;

    → ch.idle;

  end;
end;

system High_Level
  import Mid_Level_Interface (up);
  use message (value: integer)

    rename enqueue as generate,

      dequeue as add;
is
  class source is

    i: integer := 0;

  end;

  class destination is

    sum: integer := 0;

  end;

  refined generate by ... src: source is

  when ... ms.value = src.i do

    ...

    src.i := src.i +1;

  end;

  refined add by ... dst: destination is

  when ... do

    ...

    dst.sum := dst.sum + ms.value;

  end;
end; 

6 Functions

6.0.1

Functions provide a mechanism to abbreviate expressions and relations. Loops or recursion cannot be used, but special provision is made for computing the transitive closure of a relation.

(6.1)  function_definition =

function simple_name [ ( formals_list ) ] return type is

    function_body ;

end [ simple_name ] ;

6.0.2

A function may require parameters that can be of any type. Function evaluation returns a value whose type must be the one given in the function header.

6.0.3

The body of a function may use other functions defined before its definition, but it may not use itself directly or indirectly.

6.0.4

Function evaluation cannot have side effects.

6.1 Function body

6.1.1

A function body is an ordinary expression, a conditional expression, or a closure expression.

(6.2)  function_body =

expression | conditional_expression | closure_expression

(6.3)  conditional_expression =

if boolean_expression then

    function_body

{ elsif boolean_expression then

    function_body }

else

    function_body

end if

(6.4)  closure_expression =

closure boolean_expression | closure boolean_conditional_expression

6.1.2

Conditional expressions are not available outside function bodies. They shall always have else parts, and all alternative expressions shall be of the same type. A closure expression is not possible in the case of a conditional expression.

6.1.3

Boolean functions can be used to express relations. The transitive closure of such a relation can be given by a closure expression. The boolean expression in a closure expression shall be a function that has exactly two parameters of the same object type, and the result shall be boolean. Formally, if G(x,y) denotes the closure of F(x,y), then G(x,y) satisfies the recursive condition G(x,y) = F(x,y) | &eksist;z: F(x,z) & G(z,y).

6.1.4

If a function involves a closure expression or a quantified expression, or it accesses the local state of an object via a reference, either directly or indirectly through calls of other functions, it cannot be used elsewhere than in guards and global assertions.

Example 6.1 Functions and closures

class In_List (next: In_List) is

end;

function Next (left, right: In_List) return boolean is

  left.next = right;

end;

function Connected (left, right: In_List) return boolean is

  closure Next (left, right);

end;

7 Global assertions

7.0.1

Global assertions are conditions that shall be invariantly true, except in the middle of executing an action.

(7.1)  global_assertion =

assert simple_name is boolean_expression ;

7.0.2

An initial condition is a condition that has to be true immediately after the creation, but may be invalidated later.

(7.2)  global_initial_condition =

initially simple_name is boolean_expression ;

7.0.3

Assertions and initial conditions cause a run-time error, if they do not hold. They cannot have other side effects.

Example 7.0 Assertions and initial conditions

initially One_List is

  &eksist; l : In_List | ¬Connected (l, l) ::
    ∀ m : In_List | m <> l :: Connected (l, m);

assert One_List is

  &eksist; l : In_List | ¬Connected (l, l) ::
    ∀ m : In_List | m <> l :: Connected (l, m);

8 Creation

8.0.1

A system can be executed only after the creation and initialization of a world of objects by an associated creation part.

(8.1)  creation =

creation simple_name [ ( formals_list ) ] of system_simple_name is

    creation_statement_list

end [ simple_name ] ;

(8.2)  creation_statement_list =

{ creation_statement }

(8.3)  creation_statement =

procedure_definition | variable_definition | multiple_assignment 
| object_creation_statement | for_statement | conditional_statement 
| multiple_state_transition | procedure_call

8.0.2

Creation statements can use functions and classes of the associated system part.

8.0.3

Conditional statement is described in Section 4.4. A conditional statement may not involve procedure or variable definitions.

8.0.4

The parameters of a creation are given by the user when the creation is invoked.

8.0.5

Variable definitions introduce local variables for the creation part. All other types except stuff types are available. A creation variable is available immediately after its definition, and it is referenced by its simple name.

8.0.6

Quantified expressions are not allowed in creation statements.

Example 8.0 Creation

creation sample (list_length: integer) of list_example is
  a: In_List := null;

  for i in 1..list_length loop

    a := new In_List (a);

  end loop;
end sample;

8.1 Assignment

8.1.1

The syntax of multiple assignment statements is given in (4.5).

8.1.2

The expression on the right hand side may generate new objects, as described in 8.2.

8.1.3

In contrast to the system part, an assignment in a creation part can also modify the values of state and class parameters.

8.2 Object creation

8.2.1

A special statement is available for object creation.

(8.4)  object_creation_statement =

new [ ( integer_expression ) ] new_object ;

(8.5)  new_object =

class_simple_name [ ( actuals_list ) ]

8.2.2

The optional integer expression specifies the number of (identical) objects to be generated. The default is one. This number may also be specified to be infinite.

8.3 For statement

8.3.1

A for statement is available for loops in a creation part.

(8.6)  for_statement =

for control_variable_simple_name in range loop

    creation_statement_list

end loop ;

(8.7)  range =

integer_expression .. integer_expression

8.3.2

The number of iterations is expressed by the range. The control variable is assigned all values of the range in sequence, from the lower bound to the upper bound. The control variable cannot be assigned a value within the loop, but it may be used in expressions.

8.3.3

The scope of a control variable is the associated statement list. In the case of nested for statements with conflicting control variable names, inner scopes take precedence over the outer ones.

8.3.4

The statement list in a for statement shall not contain procedure or variable definitions.

8.4 Procedure definition and procedure call

8.4.1

Procedures can be defined and used in the creation part only.

8.4.2

A procedure may alter the values of its parameters. All actual parameters shall be variables. Procedures may not be recursive.

(8.8)  procedure_definition =

procedure simple_name [ ( formals_list ) ] is

    creation_statement_list

end [ simple_name ] ;

8.4.3

It is also possible to call procedures defined in other creations. The procedure must then be defined in a creation part that is associated with some system that is imported (either directly or indirectly) by the system of the current creation part. If the called procedure is not local, the creation name shall be given as a prefix in the procedure call.

(8.9)  procedure_call =

procedure_name [ ( actuals_list ) ] ;

9 Expressions

9.1 Primaries

9.1.1

Expressions are composed of primaries, which are names, function calls, constants, explicit sets, explicit sequences, or parenthesized expressions.

(9.1)  primary =

simple_primary | function_simple_name ( [ actuals_list ] ) | ( expression ) 
| new new_object | ask string | { [ set_construct ] } | ∅ 
| < [ sequence_construct ] > 

(9.2)  simple_primary =

data_name | state_name | formal_simple_name 
| creation_variable_simple_name | number | true | false |  | infinity | null 

(9.3)  string =

" { printable_character } "

(9.4)  set_construct =

simple_primary { , simple_primary } | class_simple_name

| variable_simple_name : class_simple_name '|' boolean_expression

(9.5)  sequence_construct =

simple_primary { , simple_primary }

9.1.2

For function calls, even an empty parameter list has to be given in parentheses.

9.1.3

A nonexistent object reference is expressed as null.

9.1.4

Infinity is explicitly available as a value that exceeds any other integer.

9.1.5

Sets can be given by explicit lists of elements. An empty set is denoted by an empty list or by ∅. If the set is defined by a class name, all objects of the class are included. As in 9.3.2, objects of the class can be selected by a boolean expression.

9.1.6

Sequences are given by explicit lists in angle brackets < and >. The order of the elements is significant (the first one being the leftmost), and the same element may appear several times.

9.1.7

Generators new and ask are available in the creation part only, for the generation of a new object and an integer value, respectively.

9.1.8

Printable characters are ASCII characters between space and tilde (~), except double quote (").

9.1.9

Three predefined functions exist: size, head, and tail. Size returns the number of elements in a set, sequence, or set construct, head returns the first element of a sequence, and tail returns a sequence without its first element.

Example 9.1 Primaries

  -- Infinity
"A string" -- Can only be used in connection with the generator ask
{b, d} -- A set of two elements
<a, b> -- A sequence of two elements

9.2 Operators and priorities

9.2.1

Quantification is the least binding construction for expressions. The different groups of operators are the following, listed in an ascending order of priorities:

(9.6)  quantifier =

+/ | */ | ∪/ | ∩/ | min/ | max/ | &/ | |/ | and/ | or/ | ∀ | &eksist;

(9.7)  implies =

⇒ | =>

(9.8)  logical_add_op =

| | or

(9.9)  logical_mul_op =

& | and

(9.10)  relation_op =

 = | <> | < | > | <= | >= | /= | <= | >= | ⊆ | ∈ | ∉| subset | in | not in

(9.11)  add_op =

+ | - | ∪ | &ᵶ;

(9.12)  mul_op =

* | / | mod | ∩ | min | max

(9.13)  high_precedence_operator =

¬ | not | abs | + | -

(9.14)  power = **

9.2.2

Alternative representations are given to non-ASCII symbols. For instance, or and | are synonyms. Also logical quantifier symbols ∀ and &eksist; can be used instead of &/, |/, and/, or or/.

9.2.3

Equality (=) and inequality (<>) are defined for all types and classes. Less than (<), greater than (>), less than or equal (<=), and greater than or equal (>=) are defined for integers only. The subset operator (⊆) is defined for sets; membership tests (∈ and ∉) are defined for an element and a set or sequence.

9.2.4

Set union is expressed by + or ∪, set difference by -, and set intersection by * or ∩.

9.2.5

Concatenation of sequences is expressed by &. The right operand of the operator is appended to the left operand.

9.2.6

Division (/) and modulo (mod) are defined for integers only.

9.2.7

The unary absolute value operator abs is available for integers.

9.2.8

The dyadic operations min and max for minimum and maximum are defined for integers only.

9.2.9

Power (**) is defined for integers only. The exponent has to be a non-negative number.

Example 9.2 Operator priorities

a = 3
b = 16
4 * a min 4 = 12
(a < 4 or a >= 4 and b < a) = true

9.3 Syntax of expressions

9.3.1

The syntax of expressions is the following:

(9.15)  expression =

quantifier formals_list [ '|' boolean_expression ] :: expression

| relation [ implies relation ]

(9.16)  relation =

disjunct { logical_add_op disjunct }

(9.17)  disjunct =

conjunct { logical_mul_op conjunct }

(9.18)  conjunct =

basic_expression { relation_op basic_expression }

(9.19)  basic_expression =

term { add_op term }

(9.20)  term =

factor { mul_op factor }

(9.21)  factor =

primary [ power primary ]


| high_precedence_operator primary

9.3.2

The formals of quantified expressions are restricted to object types. Quantifiers are allowed in global assertions, guards, and functions (see 6.1.4). If all values of the object type is not wanted, the set of values can be restricted by the optional boolean expression of quantified expression.

9.3.3

The optional part of a conjunct (9.16) may be repeated. In this case, each relation operator is applied to the basic expressions on its left and right, and the conjunct is equivalent to the conjunction of these relations. If the relation operator is a set or sequence membership test (∈ or ∉), exactly one optional part is required.

Example 9.3 Expressions

a.b + c
a < b < c -- Is true when the value of b is between a and c
a < b & b < c -- Equivalent to a < b < c
a = b = c -- Equivalent to a = b  &  b = c but not equivalent to a = (b = c) or (a =b) = c
a.set_variable ∪ {b, d} -- A union of sets
c.seq & <a> -- An element is added to the end of a sequence.

+/ x: C | f(x) :: 1.

9.4 Evaluation order and nonexistent components

9.4.1

Evaluation order is significant for boolean expressions. Operands are evaluated from left to right in a short circuit mode, until the value of the expression can be uniquely determined.

9.4.2

An attempt to reference an object via a null reference, or to reference a component that is nonexistent in the current state of the object, causes a run-time error in actions. Elsewhere, i.e., in guards and global assertions, this causes the smallest enclosing conjunct to evaluate to false.

10 Naming rules

10.1 Uniqueness of names

10.1.1

In a library of DisCo program units, all systems and creation parts must be named by different identifiers.

10.1.2

In each system, all classes, actions, functions, and global assertions must be named by different identifiers. Conflicts that would be caused by imported systems must be resolved by renaming. Renaming is also required if the same class has different names (because of renaming) in imported systems.

10.1.3

Within each scope in a class, all components associated with the scope shall be named with different identifiers (see 3.2.4).

10.1.4

All parameters and participants of an action shall be named by different identifiers. The scope of these consists of the action guard and body.

10.1.5

All parameters in a function definition shall be named by different identifiers. The scope of function parameters is the function body.

10.1.6

All quantified variables in a quantified expression shall be named by different identifiers. The scope of quantified variables is the boolean expression of the quantified expression.

10.1.7

All variables defined in a creation part shall be named by different identifiers. Their scope is restricted to the current creation part.

10.1.8

If the same identifier is introduced in nested scopes, the smaller enclosing scopes take precedence over the larger ones.

10.2 The structure of names

10.2.1

Prefixed names and state transitions can be used, as given in (1.5) and (4.8). Here we give a more detailed description of prefixed names that are used to reference objects, states, and data components. To distinguish this description from the above syntax, nonterminal names are used that do not appear in the syntax.

10.2.2

An object is referenced either by a simple name that has been bound to an object reference, a data name or creation variable whose value is an object reference, or by a state name that is associated with an inherited object:

(10.1)  object_reference =

formal_simple_name | data_reference | creation_variable_simple_name 
| state_reference . state_simple_name

10.2.3

The outermost state in the state hierarchy of an object is referenced by a reference to the object. A substate can be referenced by using a prefix that references its superstate.

(10.2)  state_reference =

object_reference | state_reference . state_simple_name

10.2.4

A data component can be referenced by using a prefix that identifies a state within which the component name is unique. In a creation part, the simple names of creation variables are also available.

(10.3)  data_reference =

state_reference . data_simple_name | creation_variable_simple_name

10.2.5

Within the default expressions in class definitions, all names are implicitly prefixed by a reference to the current object of that class.

10.2.6

The sequence of simple names in a state transition (see 4.3) is the same as in a state reference (10.2). There is the additional requirement that a state transition has to contain all state names for which actual parameters need be provided, and these are given immediately after the corresponding state names.

11 Multiple imports

11.0.1

Importation of systems determines a partial order between them. If system S1 is imported to S2, either directly or indirectly through other systems, S1 is called a predecessor of S2. Cyclic importation is not possible, i.e., no system can be its own predecessor.

11.0.2

In order to simplify the discussion, an auxiliary empty system E is assumed without any class or action definitions. The empty system is implicitly imported to each system that does not explicitly import any system. Two systems are called independent, if E is their only common predecessor.

11.0.3

A system shall not be imported both directly and indirectly to the same system, but it may be imported indirectly through several different systems.

11.0.4

The effect of an import clause is to form the union of the imported systems. This union is then transformed by the importing system.

11.0.5

The union of mutually independent systems consists of all the units of the component systems. In general, the union depends not only on the imported systems themselves, but also on their predecessors, as will be described below.

11.1 Classes, functions and assertions in a union

11.1.1

Two classes in different systems are considered to be the same, if and only if they are extensions of the same class, defined in one of their common predecessor systems. Notice that the same class may have different names in different imported systems (as a result of renaming), and that different classes may have the same name. Renaming is required in both cases.

11.1.2

Each class in the imported systems is taken exactly once in the union system, together with all the extensions that have been added in the imported systems or their predecessors. If different imported extensions have introduced parameters to the same state, then named association shall be used to identify them in actual parameter lists.

11.1.3

Different extensions in the imported versions of a class shall not have conflicting state or component names in the same scope.

11.1.4

The functions, global assertions, and global initial conditions of the imported systems are taken as such into the union system.

Example 11.1 Composition of class extensions

class C is        -- Original

  i: integer;

end;

extend C by        -- Extension 1

  state *idle, working, ready;

end;

extend C (... chain: C) by            -- Extension 2

end;

class C (chain: C) is          -- Parameter from extension 2

  i: integer;        -- From the original

  state *idle, working, ready;            -- From extension 1

end;

11.2 Actions in a union

11.2.1

For simplicity of description, an auxiliary empty action e with no parameters or participants and with an identically true guard is implicitly assumed to be included in each system.

11.2.2

When an action is specialized or refined, either explicitly or implicitly, the original action is called an ancestor of the specialized or refined action. The introduction of a new action is understood to be a specialization of the empty action e.

11.2.3

The actions in the union of imported systems are determined so that each of them has a unique ancestor in each of the imported systems. Conversely, each action in an imported system is an ancestor of at least one action in the union. The ancestors of the empty action are the empty actions of the imported systems.

11.2.4

When a stuff type of an imported module is refined by one or more use statements, then the module is first transformed by the associated action specializations, and the union is formed after these transformations.

11.2.5

The general ancestor relation between actions is the transitive closure of the immediate ancestor relation determined by the above rules. This relation is a partial order that is consistent with the predecessor ordering between systems. If system S1 is a predecessor of S2, then each action A2 in S2 has a unique ancestor in S1. Conversely, each action in S1 is an ancestor of at least one action in S2. In particular, the empty action e of the empty system E is an ancestor of all actions in all other systems.

11.2.6

Two actions are compatible, if they belong to different systems and their ancestors in all common predecessor systems are the same. The actions of a union system are formed so that the immediate ancestors of each action are mutually compatible, which guarantees the above properties of the ancestor relation.

11.2.7

A collection of mutually compatible actions is called minimal, if it either contains at most one non-empty action, or if replacing any one of them by the empty action would violate their mutual compatibility.

11.2.8

The ancestor relation determines a partial order between the transformations by which all actions are derived from the empty action e of the empty system E, each step (possibly) adding parameters and participants, strengthening the guard, and adding statements to the body. For a collection of mutually compatible actions these transformations are compatible in the sense that they can be combined to produce a single action, called the composition of these actions. Mutual compatibility guarantees that there are no conflicting steps in the derivations, and that the steps can be applied in any order that is consistent with their partial ordering.

11.2.9

The actions of a union system are determined as the maximal set of actions that obeys the above principles. For each collection of mutually compatible actions, with one action taken from each of the component systems, the composition of the collection is then included in the union.

11.2.10

If the immediate ancestors of an action in a union system form a non-minimal set of compatible actions, then this action is implicitly removed (i.e., its guard is strengthened to be identically false, and no name is made available for it), unless it is given as an explicit combination (see 2.3). A combination statement introduces a name for a combined action, and list all its non-empty immediate ancestors.

11.2.11

No combination statement is required if the set of immediate ancestors is minimal, but it can be used for renaming the combined action also in this case. If no combine statement is given, the name of a combined action is the concatenation of the names of its immediate ancestors, written in the order in which the predecessor systems appear in the import clause, and separated by underscores. However, if several parts of this compound name are identical, then only the first occurrences of such parts shall be included. Notice that renaming of imported actions may simplify the names of compound actions.

Example 11.2 Composition of actions