Bibliographical Notes - Dines Bjørner From Domains to Requirements

Part IV Closing

9.1 Bibliographical Notes

1. Jean-Raymond Abrial. The B Book: Assigning Programs to MeaningsandModeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge, England, 1996 and 2009.

2. Rajeev Alur and David L. Dill. A Theory of Timed Automata.Theoretical Computer Science, 126(2):183–

235, 1994. (Preliminary versions appeared in Proc. 17th ICALP, LNCS 443, 1990, and Real Time: Theory in Practice, LNCS 600, 1991).

3. Krzysztof R. Apt.Principles of Constraint Programming. Cambridge University Press, August 2003. ISBN 0521825830.

4. K. Araki et al., editors. IFM 1999–2009: Integrated Formal Methods, volume 1945, 2335, 2999, 3771, 4591, 5423 (only some are listed) ofLecture Notes in Computer Science. Springer, 1999–2009.

5. Yasuhito Arimoto and Dines Bjørner. Hospital Healthcare: A Domain Analysis and a License Language.

Technical note, JAIST, School of Information Science, 1-1, Asahidai, Tatsunokuchi, Nomi, Ishikawa, Japan 923-1292, Summer 2006.

6. C. Bachman. Data structure diagrams. Data Base, Journal of ACM SIGBDP, 1(2), 1969.

7. Alain Badiou. Being and Event. Continuum, 2005. (Lˆetre et l’´ev´enements, Edition du Seuil, 1988).

8. V. Richard Benjamins and Dieter Fensel. The Ontological Engineering Initiative (KA)2. Internet publica-tion + Formal Ontology in Informapublica-tion Systems, University of Amsterdam, SWI, Roetersstraat 15, 1018 WB Amsterdam, The Netherlands and University of Karlsruhe, AIFB, 76128 Karlsruhe, Germany, 1998.

http://www.aifb.uni-karlsruhe.de/WBS/broker/KA2.htm.

9. G. Birkhoff. Lattice Theory. American Mathematical Society, Providence, R.I., 3 edition, 1967.

10. Dines Bjørner. Software Engineering, Vol. 1: Abstraction and Modelling. Texts in Theoretical Computer Science, the EATCS Series. Springer, 2006. .

11. Dines Bjørner.Software Engineering, Vol. 1: Abstraction and Modelling; Vol. 2: Speciﬁcation of Systems and Languages; ol. 3: Domains, Requirements and Software Design. Texts in Theoretical Computer Science, the EATCS Series. Springer, 2006.

12. Dines Bjørner.Software Engineering, Vol. 2: Speciﬁcation of Systems and Languages. Texts in Theoretical Computer Science, the EATCS Series. Springer, 2006. Chapters 12–14 are primarily authored by Christian Krog Madsen.

13. Dines Bjørner. Software Engineering, Vol. 3: Domains, Requirements and Software Design. Texts in Theoretical Computer Science, the EATCS Series. Springer, 2006.

14. Dines Bjørner. Domain Engineering: Technology Management, Research and Engineering. Research Monograph (# 4); JAIST Press, 1-1, Asahidai, Nomi, Ishikawa 923-1292 Japan, This Research Monograph contains the following main chapters:

1. On Domains and On Domain Engineering – Prerequisites for Trustworthy Software – A Necessity for Believable Management, pages 3–38.

2. Possible Collaborative Domain Projects – A Management Brief, pages 39–56.

3. The Rˆole of Domain Engineering in Software Development, pages 57–72.

4. Veriﬁed Software for Ubiquitous Computing – A VSTTE Ubiquitous Computing Project Proposal, pages 73–106.

5. The Triptych Process Model – Process Assessment and Improvement, pages 107–138.

6. Domains and Problem Frames – The Triptych Dogma and M.A.Jackson’s PF Paradigm, pages 139–

175.

7. Documents – A Rough Sketch Domain Analysis, pages 179–200.

8. Public Government – A Rough Sketch Domain Analysis, pages 201–222.

9. Towards a Model of IT Security — – The ISO Information Security Code of Practice – An Incomplete Rough Sketch Analysis, pages 223–282.

10. Towards a Family of Script Languages – – Licenses and Contracts – An Incomplete Sketch, pages 283–328.

2009.

15. Dines Bjørner. From Domains to Requirements — On a Triptych of Software Development. Research Report, University of Edingburgh, November 2009.

16. Dines Bjørner. Domain Science & Engineering –From Computer Science to The Sciences of Informatics Part II of II: The Science Part. Kibernetika i sistemny analiz, (2):100–120, May 2011.

17. Dines Bjørner. Domains: Their Simulation, Monitoring and Control – A Divertimento of Ideas and Suggestions. InRainbow of Computer Science, Festschrift for Hermann Maurer on the Occasion of His 70th Anniversary., Festschrift (eds. C. Calude, G. Rozenberg and A. Saloma), pages 167–183. Springer, Heidelberg, Germany, January 2011.

18. Dines Bjørner.A Rˆole for Mereology in Domain Science and Engineering. Synthese Library (eds. Claudio Calosi and Pierluigi Graziani). Springer, Amsterdam, The Netherlands, May 2013.

19. Dines Bjørner. Domain Analysis: Endurants – A Model of Prompts [Early, incomplete draft] (paper¹, slides²). Research Report 2013-10, DTU Compute and Fredsvej 11, DK-2840 Holte, Denmark, July 2013.

20. Dines Bjørner. Domain Analysis (paper³slides⁴). Research Report 2013-1, DTU Compute and Fredsvej 11, DK-2840 Holte, Denmark, April 2013.

21. Dines Bjørner. Pipelines – a Domain Description⁵. Experimental Research Report 2013-2, DTU Compute and Fredsvej 11, DK-2840 Holte, Denmark, Spring 2013.

22. Dines Bjørner. Road Transportation – a Domain Description⁶. Experimental Research Report 2013-4, DTU Compute and Fredsvej 11, DK-2840 Holte, Denmark, Spring 2013.

23. Dines Bjørner and Cliff B. Jones, editors. The Vienna Development Method: The Meta-Language, vol-ume 61 ofLNCS. Springer, 1978.

24. Dines Bjørner and Cliff B. Jones, editors.Formal Speciﬁcation and Software Development. Prentice-Hall, 1982.

25. Dines Bjørner and Jørgen Fischer Nilsson. Algorithmic & Knowledge Based Methods — Do they “Unify” ? InInternational Conference on Fifth Generation Computer Systems: FGCS’92, pages 191–198. ICOT, June 1–5 1992.

26. Dines Bjørner, Arimoto Yasuhito, Chen Xiaoyi, and Xiang Jianwen. A Family of License Languages.

Technical report, JAIST, Graduate School of Information Science, 1-1, Asahidai, Tatsunokuchi, Nomi, Ishikawa, Japan 923-1292, August 2006.

27. Wayne D. Blizard. A Formal Theory of Objects, Space and Time. The Journal of Symbolic Logic, 55(1):74–89, March 1990.

28. Grady Booch, Jim Rumbaugh, and Ivar Jacobson.The Uniﬁed Modeling Language User Guide. Addison-Wesley, 1998.

29. Roberto Casati and Achille Varzi. Events. In Edward N. Zalta, editor, The Stanford Encyclopedia of Philosophy. Spring 2010 edition, 2010.

30. Roberto Casati and Achille C. Varzi, editors. Events. Ashgate Publishing Group – Dartmouth Publishing Co. Ltd., Wey Court East, Union Road, Farnham, Surrey, GU9 7PT, United Kingdom, 23 March 1996.

31. Peter P. Chen. The Entity-Relationship Model - Toward a Unified View of Data. ACM Trans. Database Syst, 1(1):9–36, 1976.

32. XiaoYi Chen and Dines Bjørner. Public Government: A Domain Analysis and a License Language. Tech-nical note, JAIST, School of Information Science, 1-1, Asahidai, Tatsunokuchi, Nomi, Ishikawa, Japan 923-1292, Summer 2006.

33. Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. Model Checking. The MIT Press, Five Cambridge Center, Cambridge, MA 02142-1493, USA, January 2000. ISBN 0-262-03270-8.

1 http://www.imm.dtu.dk/˜dibj/prompts-p.pdf

34. CoFI (The Common Framework Initiative). Casl Reference Manual, volume 2960 ofLecture Notes in Computer Science (IFIP Series). Springer–Verlag, 2004.

35. P. Cousot. Abstract Interpretation. ACM Computing Surveys, 28(2):324–328, 1996.

36. Krzysztof Czarnecki and Ulrich W. Eisenecker. Generative Programming: Methods, Tools, and Applica-tions. Addison Wesley, 2000.

37. Werner Damm and David Harel. LSCs: Breathing life into Message Sequence Charts. Formal Methods in System Design, 19:45–80, 2001. Early version appeared as Weizmann Institute Tech. Report CS98-09, April 1998. An abridged version appeared in Proc. 3rd IFIP Int. Conf. on Formal Methods for Open Object-based Distributed Systems (FMOODS’99), Kluwer, 1999, pp. 293–312.

38. Donald Davidson. Essays on Actions and Events. Oxford University Press, 1980.

39. J.W. de Bakker. Control Flow Semantics. The MIT Press, Cambridge, Mass., USA, 1995.

40. F. Dretske. Can Events Move? Mind, 76(479-492), 1967. reprinted in [30], pp. 415-428.

41. Ronald Fagin, Joseph Y. Halpern, Yoram Moses, and Moshe Y. Vardi. Reasoning about Knowledge. The MIT Press, Massachusetts Institute of Technology, Cambridge, Massachusetts 02142, 1996. 2nd printing.

42. David John Farmer. Being in time: The nature of time in light of McTaggart’s paradox. University Press of America, Lanham, Maryland, 1990. 223 pages.

43. Edward A. Feigenbaum and Pamela McCorduck. The ﬁfth generation. Addison-Wesley, Reading, MA, USA, 1st ed. edition, 1983.

44. John Fitzgerald and Peter Gorm Larsen.Modelling Systems – Practical Tools and Techniques in Software Development. Cambridge University Press, The Edinburgh Building, Cambridge CB2 2RU, UK, 1998.

ISBN 0-521-62348-0.

45. Martin Fowler. Domain Speciﬁc Languages. Signature Series. Addison Wesley, October 20120.

46. K. Futatsugi, A.T. Nakagawa, and T. Tamai, editors. CAFE: An Industrial–Strength Algebraic Formal Method, Sara Burgerhartstraat 25, P.O. Box 211, NL–1000 AE Amsterdam, The Netherlands, 2000.

Elsevier. Proceedings from an April 1998 Symposium, Numazu, Japan.

47. Bernhard Ganter and Rudolf Wille. Formal Concept Analysis — Mathematical Foundations. Springer-Verlag, January 1999. ISBN: 3540627715, 300 pages, Amazon price: US $ 44.95.

48. Chris W. George, Peter Haff, Klaus Havelund, Anne Elisabeth Haxthausen, Robert Milne, Claus Bendix Nielsen, Søren Prehn, and Kim Ritter Wagner.The RAISE Speciﬁcation Language. The BCS Practitioner Series. Prentice-Hall, Hemel Hampstead, England, 1992.

49. J.-C. Gr´egoire, G. J. Holzmann, and D. Peled, editors. The SPIN Veriﬁcation System, volume 32 of DIMACS series. American Mathematical Society, 1997. ISBN 0-8218-0680-7, 203p.

50. Carl A. Gunter, Elsa L. Gunter, Michael A. Jackson, and Pamela Zave. A Reference Model for Require-ments and Specifications. IEEE Software, 17(3):37–43, May–June 2000.

51. Carl A. Gunter, Stephen T. Weeks, and Andrew K. Wright. Models and Languages for Digtial Rights.

In Proc. of the 34th Annual Hawaii International Conference on System Sciences (HICSS-34), pages 4034–4038, Maui, Hawaii, USA, January 2001. IEEE Computer Society Press.

52. C.A. Gunther. Semantics of Programming Languages. The MIT Press, Cambridge, Mass., USA, 1992.

53. P.M.S. Hacker. Events and Objects in Space and Time. Mind, 91:1–19, 1982. reprinted in [30], pp.

429-447.

54. David Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8(3):231–274, 1987.

55. David Harel and Rami Marelly. Come, Let’s Play – Scenario-Based Programming Using LSCs and the Play-Engine. Springer-Verlag, 2003.

56. Dan Haywood. Domain-Driven Design Using Naked Objects. The Pragmatic Bookshelf (an imprint of

‘The Pragmatic Programmers, LLC.’), http://pragprog.com/, 2009.

57. Martin Heidegger. Sein und Zeit (Being and Time). Oxford University Press, 1927, 1962.

58. C.A.R. Hoare.Communicating Sequential Processes. C.A.R. Hoare Series in Computer Science. Prentice-Hall International, 1985. Published electronically: http://www.usingcsp.com/cspbook.pdf (2004).

59. Tony Hoare. Communicating Sequential Processes. C.A.R. Hoare Series in Computer Science. Prentice-Hall International, 1985.

60. Tony Hoare. Communicating Sequential Processes. Published electronically: http://www.usingcsp.-com/cspbook.pdf, 2004. Second edition of [59]. See alsohttp://www.usingcsp.com/.

61. G. J. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall, Englewood Cliffs, New Jersey, 1991.

62. Gerard J. Holzmann.The SPIN Model Checker, Primer and Reference Manual. Addison-Wesley, Reading, Massachusetts, 2003.

63. IEEE Computer Society. IEEE–STD 610.12-1990: Standard Glossary of Software Engineering Terminology.

Technical report, IEEE, IEEE Headquarters Office, 1730 Massachusetts Avenue, N.W., Washington, DC 20036-1992, USA. Phone: +1-202-371-0101, FAX: +1-202-728-9614, 1990.

64. ITU-T. CCITT Recommendation Z.120: Message Sequence Chart (MSC), 1992, 1996, 1999.

65. Daniel Jackson. Software Abstractions: Logic, Language, and Analysis. The MIT Press, Cambridge, Mass., USA, April 2006. ISBN 0-262-10114-9.

66. Michael Jackson. Program Verification and System Dependability. In Paul Boca and Jonathan Bowen, editors,Formal Methods: State of the Art and New Directions, pages 43–78, London, UK, 2010. Springer.

67. Michael A. Jackson. Software Requirements & Speciﬁcations: a lexicon of practice, principles and preju-dices. ACM Press. Addison-Wesley, Reading, England, 1995.

68. Michael A. Jackson. Problem Frames — Analyzing and Structuring Software Development Problems.

ACM Press, Pearson Education. Addison-Wesley, England, 2001.

69. Ivar Jacobson, Grady Booch, and Jim Rumbaugh. The Uniﬁed Software Development Process. Addison-Wesley, 1999.

70. Kyo C. Kang, SholomG. Cohen, James A. Hess, William E. Novak, and A. Spenser Peterson. Feature-Oriented Domain Analysis (FODA). Feasibility Study CMU/SEI-90-TR-021, note =, Software Engineering Institute, Carnegie Mellon University.

71. Jaegwon Kim. Supervenience and Mind. Cambridge University Press, 1993.

72. Jochen Klose and Hartmut Wittke. An automata based interpretation of Live Sequence Charts. In T. Margaria and W. Yi, editors,TACAS 2001, LNCS 2031, pages 512–527. Springer-Verlag, 2001.

73. Leslie Lamport. Specifying Systems. Addison–Wesley, Boston, Mass., USA, 2002.

74. E.C. Luschei. The Logical Systems of Le´sniewksi. North Holland, Amsterdam, The Netherlands, 1962.

75. J. M. E. McTaggart. The Unreality of Time. Mind, 18(68):457–84, October 1908. New Series. See also:

[82].

76. Neno Medvidovic and Edward Colbert. Domain-Specific Software Architectures (DSSA). Power Point Presentation, found on The Internet, Absolute Software Corp., Inc.:Abs[S/W], 5 March 2004.

77. D.H. Mellor. Things and Causes in Spacetime.British Journal for the Philosophy of Science, 31:282–288, 1980.

78. Marjan Mernik, Jan Heering, and Anthony M. Sloane. When and how to develop domain-specific lan-guages. ACM Computing Surveys, 37(4):316–344, December 2005.

79. Erik Mettala and Marc H. Graham. The Domain Specific Software Architecture Program. Project Report CMU/SEI-92-SR-009, Software Engineering Institute Carnegie Mellon University Pittsburgh, Pennsylvania 15213, June 1992.

80. Ernst-R¨udiger Olderog and Henning Dierks. Real-Time Systems: Formal Speciﬁcation and Automatic Veriﬁcation. Cambridge University Press, UK, 2008.

81. Chia-Yi Tony Pi.Mereology in Event Semantics. Phd, McGill University, Montreal, Canada, August 1999.

82. Robin Le Poidevin and Murray MacBeath, editors. The Philosophy of Time. Oxford University Press, 1993.

83. Rub´en Prieto-D´ıaz. Domain Analysis for Reusability. InCOMPSAC 87. ACM Press, 1987.

84. Rub´en Prieto-D´ıaz. Domain analysis: an introduction. Software Engineering Notes, 15(2):47–54, 1990.

85. Rub´en Prieto-D´ıaz and Guillermo Arrango. Domain Analysis and Software Systems Modelling. IEEE Computer Society Press, 1991.

86. Arthur N. Prior. Papers on Time and Tense. Clarendon Press, Oxford, UK, 1968.

87. Riccardo Pucella and Vicky Weissman. A Logic for Reasoning about Digital Rights. InProc. of the 15th IEEE Computer Security Foundations Workshop (CSFW’02), pages 282–294. IEEE Computer Society Press, 2002.

88. A. Quinton. Objects and Events.Mind, 88:197–214, 1979.

89. Wolfang Reisig. Petrinetze: Modellierungstechnik, Analysemethoden, Fallstudien. Leitf¨aden der Infor-matik. Vieweg+Teubner, 1st edition, 15 June 2010. 248 pages; ISBN 978-3-8348-1290-2.

90. John C. Reynolds. The Semantics of Programming Languages. Cambridge University Press, 1999.

91. Jim Rumbaugh, Ivar Jacobson, and Grady Booch. The Uniﬁed Modeling Language Reference Manual.

Addison-Wesley, 1998.

92. Pamela Samuelson. Digital rights management{and, or, vs.}the law.Communications of ACM, 46(4):41–

45, Apr 2003.

93. Donald Sannela and Andrzej Tarlecki.Foundations of Algebraic Semantcs and Formal Software Develop-ment. Monographs in Theoretical Computer Science. Springer, Heidelberg, 2012.

94. David A. Schmidt. Denotational Semantics: a Methodology for Language Development. Allyn & Bacon, 1986.

95. Mary Shaw and David Garlan. Software Architecture: Perspectives on an Emerging Discipline. Prentice Hall, 1996.

96. Diomidis Spinellis. Notable design patterns for domain specific languages. Journal of Systems and Software, 56(1):91–99, February 2001.

97. J.T.J. Srzednicki and Z. Stachniak, editors. Le´sniewksi’s Lecture Notes in Logic. Dordrecht, 1988.

98. S. J. Surma, J. T. Srzednicki, D. I. Barnett, and V. F. Rickey, editors. Stanis law Le´sniewksi: Collected works (2 Vols.). Dordrecht, Boston – New York, 1988.

99. Tetsuo Tamai. Social Impact of Information System Failures.Computer, IEEE Computer Society Journal, 42(6):58–65, June 2009.

100. Robert Tennent. The Semantics of Programming Languages. Prentice–Hall Intl., 1997.

101. Will Tracz. Domain-specific software architecture (DSSA) frequently asked questions (FAQ). Software Engineering Notes, 19(2):52–56, 1994.

102. Johan van Benthem.The Logic of Time, volume 156 ofSynthese Library: Studies in Epistemology, Logic, Methhodology, and Philosophy of Science (Editor: Jaakko Hintika). Kluwer Academic Publishers, P.O.Box 17, NL 3300 AA Dordrecht, The Netherlands, second edition, 1983, 1991.

103. F. Van der Rhee, H.R. Van Nauta Lemke, and J.G. Dukman. Knowledge based fuzzy control of systems.

IEEE Trans. Autom. Control, 35(2):148–155, February 1990.

104. George Wilson and Samuel Shpall. Action. In Edward N. Zalta, editor, The Stanford Encyclopedia of Philosophy. Summer 2012 edition, 2012.

105. G. Winskel.The Formal Semantics of Programming Languages. The MIT Press, Cambridge, Mass., USA, 1993.

106. J. C. P. Woodcock and J. Davies.Using Z: Speciﬁcation, Proof and Reﬁnement. Prentice Hall International Series in Computer Science, 1996.

107. JianWen Xiang and Dines Bjørner. The Electronic Media Industry: A Domain Analysis and a License Language. Technical note, JAIST, School of Information Science, 1-1, Asahidai, Tatsunokuchi, Nomi, Ishikawa, Japan 923-1292, Summer 2006.

108. Chao Chen Zhou and Michael R. Hansen.Duration Calculus: A Formal Approach to Real–time Systems.

Monographs in Theoretical Computer Science. An EATCS Series. Springer–Verlag, 2004.

Appendices

Abstraction & Modelling – using RAISE

⁶³⁰

A.1 RSL: The Raise Specification Language

⁶³¹

A.1.1 Type Expressions

Type expressions are expressions whose value are type, that is, possibly infinite sets of values (of “that”

type).

Atomic Types

Atomic types have (atomic) values. That is, values which we consider to have no proper constituent (sub-)values, i.e., cannot, to us, be meaningfully “taken apart”.

RSLhas a number of built-in atomic types. There are the Booleans, integers, natural numbers,

reals, characters, and texts. ⁶³²

type

[1]Bool true,false

[2]Int ... ,−2,−2, 0, 1, 2,...

[3]Nat 0, 1, 2,...

[4]Real ...,−5.43,−1.0, 0.0, 1.23· · ·, 2,7182· · ·, 3,1415· · ·, 4.56,...

[5]Char ”a”, ”b”,..., ”0”,...

[6]Text ”abracadabra”

Composite Types ⁶³³

Composite types have composite values. That is, values which we consider to have proper con-stituent (sub-)values, i.e., can be meaningfully “taken apart”. There are two ways of expressing composite types: either explicitly, using concrete type expressions, or implicitly, using sorts (i.e.,

abstract types) and observer functions. ⁶³⁴

Concrete Composite Types

From these one can form type expressions: ﬁnite sets, inﬁnite sets, Cartesian products, lists, maps, etc.

LetA,BandCbe any type names or type expressions, then:

[ 7 ] A-set [ 8 ] A-infset

[ 9 ] A×B×...×C [ 10 ] A^∗

[ 11 ] A^ω

[ 12 ] A →m B [ 13 ] A→B [ 14 ] A→^∼ B [ 15 ] (A)

[ 16 ] A|B| ...|C

[ 17 ] mk id(sel a:A,...,sel b:B) [ 18 ] sel a:A... sel b:B

The following are generic type expressions:

301. The Boolean type of truth valuesfalseandtrue.

302. The integer type on integers ..., –2, –1, 0, 1, 2, ... .

303. The natural number type of positive integer values 0, 1, 2, ...

304. The real number type of real values, i.e., values whose numerals can be written as an integer, followed by a period (“.”), followed by a natural number (the fraction).

305. The character type of character values ^′′a^′′,^′′b^′′, ...

306. The text type of character string values^′′aa^′′,^′′aaa^′′, ...,^′′abc^′′, ...

307. The set type of ﬁnite cardinality set values.

308. The set type of inﬁnite and ﬁnite cardinality set values.

309. The Cartesian type of Cartesian values.

310. The list type of ﬁnite length list values.

311. The list type of inﬁnite and ﬁnite length list values.

312. The map type of ﬁnite deﬁnition set map values.

313. The function type of total function values.

314. The function type of partial function values.

315. In(A) Ais constrained to be:

• either a CartesianB×C×... ×D, in which case it is identical to type expression kind 9,

• or not to be the name of a built-in type (cf., 1–6) or of a type, in which case the paren-theses serve as simple delimiters, e.g.,(A →m B), or (A^∗)-set, or (A-set)list, or(A|B) →m

(C|D|(E→mF)), etc.

316. The postulated disjoint union of typesA, B,. . . , andC.

317. The record type of mk id-named record valuesmk id(av,...,bv),whereav,. . . ,bv,are values of respective types. The distinct identiﬁerssel a,etc., designate selector functions.

318. The record type of unnamed record values(av,...,bv),whereav,. . . ,bv,are values of respective types. The distinct identiﬁerssel a,etc., designate selector functions.

635

Sorts and Observer Functions type

A, B, C,..., D value

obs B: A→B, obs C: A→C,..., obs D: A→D

The above expresses that values of type A are composed from at least three values — and these are of type B, C, . . . , and D. A concrete type deﬁnition corresponding to the above presupposing material of the next section

type

B, C,..., D

A = B ×C×...×D

A.1.2 Type Definitions ⁶³⁶ Concrete Types

Types can be concrete in which case the structure of the type is speciﬁed by type expressions:

type

A = Type expr

Some schematic type deﬁnitions are:

[ 1 ] Type name = Type expr/∗ without|s or subtypes∗/

[ 2 ] Type name = Type expr 1|Type expr 2| ...|Type expr n [ 3 ] Type name ==

mk id 1(s a1:Type name a1,...,s ai:Type name ai)| ...|

mk id n(s z1:Type name z1,...,s zk:Type name zk) [ 4 ] Type name :: sel a:Type name a ... sel z:Type name z [ 5 ] Type name ={|v:Type name^′^• P(v) |}

where a form of [2–3] is provided by combining the types: 637

Type name = A|B|...|Z A == mk id 1(s a1:A 1,...,s ai:A i) B == mk id 2(s b1:B 1,...,s bj:B j) ...

Z == mk id n(s z1:Z 1,...,s zk:Z k)

TypesA, B, ..., Zare disjoint, i.e., shares no values, provided allmk id kare distinct and due to the use of the disjoint record type constructor ==.

axiom

∀ a1:A 1, a2:A 2,..., ai:Ai^•

s a1(mk id 1(a1,a2,...,ai))=a1∧s a2(mk id 1(a1,a2,...,ai))=a2∧ ...∧s ai(mk id 1(a1,a2,...,ai))=ai∧

∀ a:A^• letmk id 1(a1^′,a2^′,...,ai^′) = ain

a1^′= s a1(a)∧a2^′= s a2(a)∧...∧ai^′= s ai(a)end

Subtypes ⁶³⁸

InRSL, each type represents a set of values. Such a set can be delimited by means of predicates.

The set of valuesbwhich have type Band which satisfy the predicateP, constitute the subtype A:

type

A ={|b:B^•P(b)|}

Sorts — Abstract Types ⁶³⁹

Types can be (abstract) sorts in which case their structure is not speciﬁed:

type

A, B,..., C

A.1.3 The RSLPredicate Calculus ⁶⁴⁰ Propositional Expressions

Let identiﬁers (or propositional expressions)a, b, ..., cdesignate Boolean values (trueorfalse[or chaos]). Then:

false,true

a, b,..., c∼a, a∧b, a∨b, a⇒b, a=b, a6=b

are propositional expressions having Boolean values.∼,∧,∨,⇒, = and6= are Boolean connectives (i.e., operators). They can be read as:not,and,or,if then (orimplies),equal andnot equal.

Simple Predicate Expressions ⁶⁴¹

Let identiﬁers (or propositional expressions)a, b, ..., cdesignate Boolean values, letx, y, ..., z(or term expressions) designate non-Boolean values and leti, j,. . ., kdesignate number values, then:

false,true a, b,..., c

∼a, a∧b, a∨b, a⇒b, a=b, a6=b x=y, x6=y,

i<j, i≤j, i≥j, i6=j, i≥j, i>j are simple predicate expressions.

Quantified Expressions ⁶⁴²

LetX, Y,. . ., Cbe type names or type expressions, and letP(x),Q(y) andR(z) designate predicate expressions in whichx, y andz are free. Then:

∀ x:X^•P(x)

∃ y:Y^•Q(y)

∃ ! z:Z^•R(z)

are quantiﬁed expressions — also being predicate expressions.

They are “read” as: For all x (values in type X) the predicate P(x) holds; there exists (at least) one y (value in type Y) such that the predicate Q(y) holds; and there exists a unique z (value in typeZ) such that the predicateR(z) holds.

A.1.4 Concrete RSLTypes: Values and Operations 643

Arithmetic type

Nat,Int,Real value

+,−,∗:Nat×Nat→Nat |Int×Int→Int|Real×Real→Real /:Nat×Nat→Nat^∼ |Int×Int→Int^∼ |Real×Real→Real^∼

<,≤,=,6=,≥,>(Nat|Int|Real)→(Nat|Int|Real)

Set Expressions ⁶⁴⁴ Set Enumerations

Let the belowa’s denote values of typeA, then the below designate simple set enumerations:

{{},{a},{e1,e2,...,en},...} ∈A-set

{{},{a},{e1,e2,...,en},...,{e1,e2,...}} ∈A-infset

645

Set Comprehension

The expression, last line below, to the right of the≡, expresses set comprehension. The expression

“builds” the set of values satisfying the given predicate. It is abstract in the sense that it does not do so by following a concrete algorithm.

type A, B

P = A→Bool Q = A→^∼ B value

comprehend: A-infset×P×Q→B-infset comprehend(s,P,Q)≡ {Q(a)|a:A^• a∈s∧P(a)}

Cartesian Expressions ⁶⁴⁶

Cartesian Enumerations

Leterange over values of Cartesian types involvingA,B,. . .,C, then the below expressions are simple Cartesian enumerations:

type

A, B,..., C A×B×... ×C value

(e1,e2,...,en)

List Expressions ⁶⁴⁷

List Enumerations

Letarange over values of typeA, then the below expressions are simple list enumerations:

{hi, hei,...,he1,e2,...,eni,...} ∈A^∗

{hi, hei,...,he1,e2,...,eni,...,he1,e2,...,en,...i,...} ∈A^ω ha i ..a j i

The last line above assumesai andaj to be integer-valued expressions. It then expresses the set of integers from the value of ei to and including the value ofej. If the latter is smaller than the

former, then the list is empty. 648

List Comprehension

The last line below expresses list comprehension.

type

A, B, P = A→Bool, Q = A →^∼ B value

comprehend: A^ω ×P×Q→^∼ B^ω comprehend(l,P,Q)≡

hQ(l(i)) |iinh1..lenli^•P(l(i))i

Map Expressions 649

Map Enumerations

Let (possibly indexed)uandv range over values of typeT1 andT2, respectively, then the below

In document Dines Bjørner From Domains to Requirements (Sider 139-0)