• Ingen resultater fundet

Discrete and Continuous Entities

1.7 The Entity, Operation, Event and Behaviour Paradigm

1.7.1 Discrete and Continuous Entities

The concepts of discrete and continuous are closely interwoven and are mainly, or best, understood in a physical context. From Wikipedia5 we bring: Dis-creteness constituting a separate thing; consisting of non-overlapping, but possibly adjacent, butdistinct parts. Discreteness are fundamentally discrete in the sense of not supporting or requiring the notion of continuity. Conti-nuity is seen as consistency, over time, of the characteristics of persons, plot, objects, places and events as observed.

An Analysis slide 67

For our purposes we shall limit our consideration of entity discreteness and continuity to the physically, more specifically tactile manifested forms: if a

5Wikipedia was, around 2009The Internet-basedFree Encyclopedia.

invisible

Dines Bjorner: 1st DRAFT: January 2, 2009

1.7 The Entity, Operation, Event and Behaviour Paradigm 17 physical, simple entity is fixed, that is does not change physical, spatial form, then we shall consider it a discrete, simple entity; if, instead, a physical, simple entity is liquid or gaseous, that is can, say through the force of gravity, change physical, spatial form, then we shall consider it a continuous, simple entity.

Structures slide 68

Let us try encircle these concepts. To do so we introduce a notion of entity structure.

Characterisation 24 (Entity Structure) By the structure of an entity we understand how that entity is “made up”, whether a simple entity, opera-tion, event or behaviour; whether atomic, composite or continuous; whether static:fixed number of possible subentities and/or possible attributes, or dy-namic:variable number of possible subentities and/or possible attributes.

slide 69

Observations

Note that the values of attributes and the number of alike sub-entities of composite entities may change while the structure remains the same. Thus the structure concept implies that if two or more simple entities, or one simple entity over time, has the same, fixed, invariant structure but with possibly changing values of attributes or changing number of sub-entities, then they are discrete, simple entities. We (forward) refer to appendix example Sect. E.1.2

on page 172. It follows up on this methodology concept. slide 70 Finite Structures

A simple entity structure is finite if it is either atomic or, if composite, then consists of a finite number of finite subentities, or, if continuous, its measure of “size”, i.e., its amount of substance, or, if time, is finite.

Characterisations slide 71

Characterisation 25 (Discrete) Being discrete is a property associated with entities.

An entity is discrete if it is timewise fixed, i.e., does not change spatial ex-tent with time but could change value of possible sub-entities or of attributes.

Characterisation 26 (Continuous) Being continuous is a property asso-ciated with entities. An entity is continuous if it is timewise variable, i.e., can change spatial extent with time, or if any subpart of it is also an entity of the same structure.

invisible

Dines Bjorner: 1st DRAFT: January 2, 2009

18 1 The Triptych Paradigms

Examples slide 72

Our examples will be taken from the physical world as observed by physicists6. They are7:

• amount of (chemical) substance (Mol))8.

slide 73

Analysis of Time

There is a slight problem with thetime example. There isabsolute time and there isrelative time.Byabsolute time we understandtime since some “point in time”. Byrelative time we understand atime interval between twotimes, i.e., two ‘points in time’. The difference between these concepts can, perhaps,

slide 74

best be understood in terms of the operations that one can perform on them:

One can compare twoabsolute timesin order to find out whichabsolute time is the later (earlier); and one can compare tworelative times in order to find out which time interval is larger of the two. One cannot add two absolute times, but one can addtime intervals. One can subtract twoabsolute times, one, a smaller, from the other, the larger, to obtain the elapsedtime interval.

And so forth. In practice absolute times are abstracted as time and relative

slide 75

time are abstracted as time intervals; and both are abstracted in terms of continuous quantities (reals,Real). In practice absolute time is concretised

slide 76

in terms of date (year (AD), month (Jan., Feb., . . . , Dec.), day of month (1, 2, . . . , 28, 29, 30 or 31)) and hour (0, 1, . . . , 23), minute (0, 1, 2, . . . , 59) and second (0, 1, 2, . . . , 59)); and relative time is concretised in terms of number of elapsed years, months, days, hours, minutes and seconds; and these are expressed in terms of discretised quantities (say natural numbers).

We refer to Exercises 1.10.20 on page 36 and 1.10.21 on page 36.

6http://en.wikipedia.org/wiki/SI

7For each of the seven SI units we state its general (class) name and, in parentheses, the sort (i.e., type) name and, initalic, commonly used (textbook) abbreviations.

8The SI unit for amount of substance is the mole (type name: mol), which is defined as the amount of substance that has an equal number of elementary entities as there are atoms in 12gofcarbon-12. That number is equivalent to (but not defined as) the Avogadro constant,NA, which has a value of 6.022141791023 mol1.

invisible

Dines Bjorner: 1st DRAFT: January 2, 2009

1.7 The Entity, Operation, Event and Behaviour Paradigm 19

1.7.2 Entity Classification slide 77

We shall now present a classification of simple entities. This classification shall serve and serves our purposes. The classification is not claimed to constitute a scientific theory or fact. But it is claimed to reflect our engineering approach to modelling.

The classification of simple entities partition their universe into three parts.

• continuous simple entities,

• atomic simple entities and

• composite simple entities.

slide 78

The classification allows composite simple entities to be composed from suben-tities that are either continuous or atomic or themselves composite. So it is not a matter of a simple entity which is not continuous instead being discrete.

A discrete simple entity is an entity which is not continuous, and, if composite, then all of its subentities are discrete simple entities. Since all simple entities are of finite structure the above recursive characteristation stops.

1.7.3 Simple Entities slide 79

We (forward) refer to appendix example Sect. C.5 on page 164. It follows up on this methodology concept.

Characterisation 27 (Simple Entity) By asimple entity we mean some-thing we can point to, i.e., somesome-thing manifest, or a concept abstracted from, such a phenomenon or concept thereof.

Simple entities are either continuous, atomic or composite. The decision as to which simple entities are considered continuous, atomic or composite is a decision sˆolely taken by the describer.

Atomic Simple Entities slide 80

Characterisation 28 (Atomic Simple Entity) By anatomic simple en-tity we intuitively understand a simple entity which “cannot be taken apart”

(into other, the sub-entities) and which possess one or more attributes.

Attributes — Types and Values slide 81

With any entity we can associate one or more attributes.

Characterisation 29 (Attribute) By anattribute we understanda pair of a typeand avalue.

slide 82

invisible

Dines Bjorner: 1st DRAFT: January 2, 2009

20 1 The Triptych Paradigms

Example 1 (Atomic Entities)

Entity:Person Entity:Bank Account

Type Value Type Value

Name Dines Bjørner number 212 023 361 918 Weight 118 pounds balance 1,678,123 Yen

Height 179 cm interest rate 1.5 %

Gender male credit limit 400,000 Yen

.

“Removing” an attribute from an entity destroys its “entity-hood”.

Composite Entities slide 83

Characterisation 30 (Composite Entity) By acomposite entitywe intu-itively understand an entity (i) which “can be taken apart” into sub-entities, (ii) where the composition of these is described by its mereology, and (iii) which, apart from the attributes of the sub-entities, further possess one or more attributes.

Sub-entities are entities.

Mereology slide 84

Characterisation 31 (Mereology) Bymereology we understanda theory of part-hood relations. That is, of the relations of part to whole and the relations of part to part within a whole.

The term mereology seems to have been first used in the sense we are using it by the Polish mathematical logician Stanis law Leshniewski [127, 138, 176, 177, 183].

Mereology:“set” of one or mores(egment)s and

“set” of two or morej(unction)s

such that eachs(egment) is delimited by twoj(unctions) and such that each j(unction) connects one or mores(egments) Attributes

invisible

Dines Bjorner: 1st DRAFT: January 2, 2009

1.7 The Entity, Operation, Event and Behaviour Paradigm 21

slide 86

To put the above example of a composite entity in context we give an example

of both an informal narrative and a corresponding formal specification: slide 87 Example 3 (Transport Net, A Formalisation) A transport net consists

of one or more segments and two or more junctions. With segments [junctions]

we can associate the following attributes: segment [junction] identifiers, the identifiers of the two junctions to which segments are connected [the identifiers of the one or more segments connected to the junction], the mode of a segment

[the modes of the segments connected to the junction] slide 88 type

Si, Ji, M, Nm, Co, Ye are not entities. They are names of attribute types and, as such, designate attribute values. N is composite, S and J are considered atomic .

States slide 89

Characterisation 32 (State) By a domainstatewe shall understand a col-lection of domain entities chosen by the domain engineer.

The pragmatics of the notion of state is that states are recurrent arguments to functions and are changed by function invocations.

Formal Modelling of Simple Entities slide 90 The Basics

How do we model entities ? The answer is: by selecting a name for the desired

“set”, that is, type of entities; by defining that type to be either an abstract type, i.e., a sort,

invisible

Dines Bjorner: 1st DRAFT: January 2, 2009

22 1 The Triptych Paradigms type

A

or a concrete type, i.e., with defined, concrete values.

type

A = Type Expression

slide 91

Values of the type are then expressed as:

value a:A

As our main support example unfolds in Appendices A–N we shall illus-trate sorts with their observer, generator and classifier functions and concrete types over either basic types (Booleans,Integers,Natural numbers,Reals, etc., or over composite types (sets, Cartesians, records, lists, maps, functions).

Appendix Sect. O.2 (Pages 292–296) gives a terse introduction to the type sys-tem of our main formal specification languageRSL.

slide 92

Some Caveats

This section has dealt with discreteandcontinuous,andatomicand compos-ite simple entities. where composite simple entities possessed subentities,a mereology of these, andattributes. We can (and must) express these distinc-tions (i.e., properties) of domains clearly in narratives, but cannot do so in our chosen, or for that matter in any formal specification language !

slide 93

Thus we shall, without discrimination, use theRSLtype system to express both the possible subentity types of composite types and the attributes of these composite types. Whether a type is continuous, discrete or composite will only transpire rather indirectly from the formulas: in the form, for exam-ple, of observer functions, but these will not discriminate between observing attributes or subentities.

slide 94

One could, of course, extend the (or any) formal specification language with the following literals (allowing plural forms): attribute, subentity, discrete, continuous, atomic and composite. These could be used, for example, in the following type expressions:

Etcetera. We shall consider all such use of the literals as pragmas, that is, as pragmatic comments. Their presence (or absence) has no semantic impor-tance.

invisible

Dines Bjorner: 1st DRAFT: January 2, 2009

1.7 The Entity, Operation, Event and Behaviour Paradigm 23

Discussion slide 95

Simple Entities, Operations, Events and Behaviours as Entities

We have focused in this section on a concept of simple entities. We have used the prefix ‘simple’ since we consider the totality of simple entities, operations, events and behaviours to all be entities. As entities they are potentially arguments of operations, events and behaviours. We shall not here pursue

this possibility further. slide 96

A Possible Critique of Our ‘Simple Entity’ Ontology

We advice the reader that the concepts of discrete and continuous, and attribute and subentities, and atomic and composite are “non-standard”, i.e., not commonly accepted or in widespread usage. The reader might have guessed that from the “Some Caveats” paragraphs. Nevertheless we bring

them here in textbook form since we think that they are indeed useful. slide 97 We also remind the reader that the concepts of, for example, physical types:

meter,kilogram,second,Ampere,Kelvin,candelaandmol and their derivatives as part of a specification language is not new, it was the subject of a number of (different) chapter exercises in Vol.2 of my book: and of a MSc.

Thesis project in the late 1990s. Add to this “applied science” typology one slide 98 of “business” typology Danish Kroner, Euro, revenue, expense,

bud-get,debit,credit,spent,committed,asset,liability,account,balance sheet, general ledger,balance, sales,accounts receivable,inventory, etc., etc., and you have exciting new projects in the design and implementation of domain specific programming languages that allow the separate definition of application specific type systems, of corresponding scale and conversion systems (millimeter, centimeter, meter, kilometer, inch, foot, yard, mile), etc.,

and of axioms that govern laws of physics, or laws of accounting, etc. slide 99

slide 100–101

1.7.4 Operations slide 102

We can, from a pragmatic viewpoint, distinguish between several classes of domain operations: (i) There are the operations that a stakeholder in the domain apply to one or more simple entities of the domain state in order to change that state (we shall refer to these operations as state-changing operations); (ii) there are the operations that a stakeholder in the domain apply to a simple entity of the domain state and in order to observe a property of that entity or “extract” a value of an attribute of that entity (we shall refer to these operations as state-observing or extracting operations); and (iii) there are the operations that a stakeholder in the domain apply to results of having applied state-observing or extracting operations in order to ascertain (“calculate”) values of domain concepts.

We (forward) refer to appendix example Sect. C.6 on page 164. It follows up on this methodology concept.

invisible

Dines Bjorner: 1st DRAFT: January 2, 2009

24 1 The Triptych Paradigms

Characterisations slide 103

Characterisation 33 (Operation) By an operation we shall understand something (i.e., a function) which when applied to what we shall call ar-guments (i.e., entities) yield some entities called the result of the function (application).

slide 104

The observer functions of the formal example above are not the kind of func-tions we are (later) seeking to identify in domains. These observer funcfunc-tions are mere technicalities: needed, due to the way in which we formalise — and are deployed in order to express sub-entities, mereologies and attributes.

Describing Operations slide 105

One can describe functions in a variety of ways. We shall briefly mention four:

“direct” definitions,pre/postcondition definitions, “mixtures” of the former two, and axiomatically. Each of these can be formulated either informally or formally. But first we introduce the concepts of operation (or function) signatures and of actions and their signatures.

Operation Signatures slide 106

Characterisation 34 (Operation Signature) By a operation signature we mean thenameandtype of a operation.

type

A, B, ..., C, X, Y,.., Z value

f: A×B×... ×C→X×Y×... ×Z

The last line above expresses a schematic operation signature. Narratively, it expresses that the functionf takes ordered arguments of the typesA, B, ..., C and yields results of the (Cartesian) typeX×Y×...×Z.

Actions slide 107

Characterisation 35 (Action) By anactionwe shall understand the same thing as applying a state-changing operation (function) to its arguments (in-cluding the state).

Action Signatures

One can speak of three kinds of actions, and hence of action signatures. Let Σ denote the type of states.

slide 108

invisible

Dines Bjorner: 1st DRAFT: January 2, 2009

1.7 The Entity, Operation, Event and Behaviour Paradigm 25 type

Valuation functions inspect the state, do not change it, and yield a value.

Interpretation functions inspect the state, change it, but do not yield a (fur-ther) value. Elaboration functions inspect the state, change it, and yield a

value. slide 109

Operation Definitions

Characterisation 36 (Operation Definiton) By an operation definition we mean an operation signature and something which describes the relation-ship between operation arguments (the a:A’s, b:B’s, . . . , c:C’s and the x:X’s, y:Y’s, . . . , z:Z’s).

slide 110

Example 4 (Well Formed Routes) Presupposing material presented in Example 3 on page 21: The last line above describes the route wellformedness predicate. The meaning of the “(,,” and “,,)” is that the omitted path components “play no rˆole”

slide 111

Direct Operation Definitions

In a narrative direct operation definition the signature is described followed by an abstracted description of the operation, for example:“Operationf applies to arguments,a, of typeA, and yields results,bor type B.” “Operationf, when

applied to argumenta, i.e.,f(a), yields a result,b, which arises as follows ...” slide 112 Example 5 (The Factorial Function Definition: Direct) Informally and direct formally:

1. The factorial function applies to natural numbers and yields natural numbers.

The factorial function is otherwise defined as follows:

invisible

Dines Bjorner: 1st DRAFT: January 2, 2009

26 1 The Triptych Paradigms

2. Applied to the natural number 0 it yields the natural number 1.

Applied to the natural numbern(larger than 0) it yields 3. Applied to the natural numbern(larger than 0) it yields

(a) the result of multiplying the numbern

(b) with the result of applying the factorial function ton−1.

value

1 fact:Nat →Nat

2–3 fact(n) ≡ifn=0 then1elsen∗fact(n−1) end .

slide 113

A formal, direct function definition, including the function signature thus looks like this ‘schematic’:

value f: A→B f(a)≡ C(a)

Here A and B are some type clauses; C is some clause: some (process) ex-pression, some (process) statement usually with a free identifier, say x, and C(a) designates the evaluation of that clause with the argumentabound to all occurrences of the free identifierx.

slide 114

Pre/Post Operation Definitions

In a narrativepre/post operation definition the signature is described fol-lowed by an abstracted description ofpre/postconditions of the operation, for example: “Operation f applies to arguments, a, of type A, and yields re-sults,b or typeB.” “Operationf, when applied to argumenta, i.e.,f(a), yields a result, let us call it b; “A pre condition of a is that it satisfies the following predicate: ... , etc.” “The relation between proper input argumentsaand results, bis expressed by thepostcondition: ..., etc.”

slide 115

Example 6 (Factorial Function Definition: pre/post) Informally and for-mally: Narrative:The factorial function applies to natural numbers and yields natural numbers. The factorial function is otherwise characterised as follows: Let the factorial ofnbe calledn;nmust be larger than or equal to0;n= 0implies that the factorial of n is 1; n>0 implies that the factorial ofn is the result of multiplying the number n with the result of applying the factorial function to n−1.Formalisation:

invisible

Dines Bjorner: 1st DRAFT: January 2, 2009

1.7 The Entity, Operation, Event and Behaviour Paradigm 27 .

slide 116

A pre/post operation definition, including the function signature looks like this ‘schematic’:

HereAandBare some type clauses;P is some predicate expression with free identifier, sayx;Qis some predicate expression with free identifiers, sayy, z;

P(a) designates the evaluation of the predicate with the argumentabound to all occurrences of the free identifierx; andQ(a, b) designates the evaluation of the predicate with the argumentsa, bbound to all occurrences of respecxtive

free identifiers yandz. slide 117

“Mixed” Operation Definitions

In a narrative, mixed operation definition the signature is described — usually involving arguments (and possibly also results) types that denote “larger”

sets of values than actually accepted (respectively yielded). followed by an abstracted description of the operation, for example:“Operationf applies to arguments, a, of typeA, and yields results, b or type B.” “Operation f, when applied to argument a, i.e.,f(a), yields a result,b, which arises as follows ...”;

followed, finally, by apre condition (on the operation input arguments). slide 118 Example 7 (Factorial Function Definition: “Mixed”) Informally and for-mally: Narrative:The factorial function applies to integers and yields natural numbers. The factorial function is otherwise characterised as follows: 5 on page 25

Formalisation:

value

fact:Int→Nat

fact(n) ≡ifn=0 then1 elsen∗fact(n−1) end pre: n≥0

.

slide 119

A formal, “mixed” operation definition, including the function signature thus looks like this ‘schematic’:

value f: A→B f(a)≡ C(a)

pre:P(a)

invisible

Dines Bjorner: 1st DRAFT: January 2, 2009

28 1 The Triptych Paradigms

Here A and B are some type clauses; C is some clause: some (process) ex-pression, some (process) statement usually with a free identifier, sayx; C(a) designates the evaluation of that clause with the argument a bound to all occurrences of the free identifierx;P is some predicate expression with free identifier, sayx; andP(a) designates the evaluation of the predicate with the argumentabound to all occurrences of the free identifierx.

slide 120

Axiomatic Operation Definitions

Example 8 (Factorial Function Definition: axiomatic) Informally and formally:Narrative:The factorial function, together with natural numbers sat-isfy the following two axioms: factorial of 0 is 1, and factorial ofn, for n larger than0, is n multiplied by the factorial ofn−1.Formalisation:

value

Formal axiomatic operation definitions thus looks like this ‘schematic’:

Formal axiomatic operation definitions thus looks like this ‘schematic’: