Abstract
SPECTRAL is an experiment in specification language design that tries to maintain compactness in spite of a number of orthogonal concepts. The design is based on Extended ML and PROSPECTRA, generalising and extending both approaches. Of particular concern are the means for structuring specifications and programs in-the-large and in-the-small. The language includes constructs for defining general higher-order functions yielding specifications or program modules. Concepts of subtyping and (object-oriented) inheritance are included to support the specification development process and to enhance re-usability. Much of the power of the language comes from the use of dependent types.
The work reported in this paper has been partially supported by the Commission of the European Communities in the ESPRIT Basic Research Working Group COMPASS, and a grant from the UK Science and Engineering Research Council
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
R. Burstall and J.A. Goguen: Putting theories together to make specifications. Proc. 5th Intl. Joint Conf. on Artificial Intelligence, Cambridge, Mass., 1045–1058 (1977).
M. Broy: An example for the design of distributed systems in a formal setting: the lift problem. Universität Passau, Tech. Rep. MIP 8802 (1988).
M. Broy: Towards a design methodology for distributed systems, in: M. Broy (ed.):: Constructive Methods in Computing Science. NATO ASI Series F55, Springer (1989) 311–364.
A. Blikle and A. Tarlecki: Naive denotational semantics. Information Processing '83. North-Holland (1983).
L. Cardelli, G. Longo: a semantic basis for Quest. Digital Systems Research Center, Palo Alto, Tech. Rep. No. 55 (1990). (extended abstract in Proc. ACM Conf. on Lisp and Functional Programming, Nice June 1990).
S. Clerici and F. Orejas: GSBL: an algebraic specification language based on inheritance. Proc. 1988 European Conf. on Object Oriented Programming, Oslo. LNCS 322, 78–92 (1988).
M. Bidoit, H.-J. Kreowski, F. Orejas, P. Lescanne and D. Sannella (eds.): A comprehensive algebraic approach to system specification and development: Annotated Bibliography. LNCS, to appear (1991).
R. Constable et al: Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall (1986).
O.-J. Dahl, B. Myrhaug and K. Nygaard: Simula 67 common base language. Report S-22, Norwegian Computing Center, Oslo (1970); revised edition (1984).
S. Finn and M. Fourman: LAMBDA logic manual. Draft Report, Abstract Hardware Ltd. (1990).
J.S. Fitzgerald and C.B. Jones: Modularizing the formal description of a database system. Proc. VDM'90 Conference, Kiel. LNCS 428 (1990).
J.A. Goguen and R. Burstall: Introducing institutions. Proc. Logics of Programming Workshop, Carnegie-Mellon. LNCS 164, 221–256 (1984).
J.V. Guttag and J.J. Horning: Report on the Larch shared language. Science of Computer Programming 6 (2), 103–134 (1986).
J.A. Goguen, J.-P. Jouannaud and J. Meseguer: Operational semantics of order-sorted algebra. Proc. 12th Intl. Conf. on Automata, Languages and Programming, Nafplion, Greece. LNCS 194 (1985).
J.A. Goguen and J. Meseguer: Order-sorted algebra solves the constructor-selector, multiple representation and coercion problems. Proc. 2nd IEEE Symp. on Logic in Computer Science, Cornell (1987).
J.A. Goguen: Parameterized programming. IEEE Trans. Software Engineering SE-10, 528–543 (1984).
R. Harper: Introduction to Standard ML. Report ECS-LFCS-86-14, Univ. of Edinburgh. Revised edition (1989).
B. Krieg-Brückner: Algebraic specification and functionals for transformational program and meta program development. in Díaz, J., Orejas, F. (eds.): Proc. TAPSOFT '89 (Barcelona), Vol. 2. LNCS 352 (1989) 36–59.
B. Krieg-Brückner: PROgram development by SPECification and TRAnsformation. Technique et Science Informatiques: Advanced Software Engineering in ESPRIT (special issue) (1990) 134–149
B. Krieg-Brückner (ed.): PROgram development by SPECification and TRAnsformation: Vol. I: Methodology, Vol. II: Language Family, Vol. III: System. PROSPECTRA Reports M.1.1.S3-R-55.2,-56.2,-57.2. Universität Bremen, 1990. (to appear in LNCS).
B. Lampson and R. Burstall: Pebble, a kernel language for modules and abstract types. Information and Computation 76, 278–346 (1988).
T. Lehmann and J. Loeckx: The specification language of OBSCURE. in: D. Sannella (ed.): Selected Papers of the 5th Workshop on Specification of Abstract Data Types, Gullane, Scotland. LNCS 332, 131–153 (1988).
D. MacQueen: Modules for Standard ML. In: Report ECS-LFCS-86-2, Univ. of Edinburgh (1986).
D. MacQueen: Using dependent types to express modular structure. Proc. 13th ACM Conf. on Principles of Programming Languages, 277–286 (1986).
B. Meyer: Object-Oriented Software Construction. Prentice-Hall (1988).
J. Meseguer and J.A. Goguen: Initiality, induction and computability. Algebraic Methods in Semantics (M. Nivat and J. Reynolds, eds.), 459–540. Cambridge Univ. Press (1985).
J. Mitchell and R. Harper: The essence of ML. Proc. 15th ACM Conf. on Principles of Programming Languages, 28–46 (1988).
J. Mitchell, S. Meldal, N. Madhav and D. Katiyar: An extension of Standard ML modules with subtyping and inheritance (extended abstract). Draft report, Stanford University (1990). to appear in Proc. ACM Conf. on Principles of Programming Languages (1991)
R. Milner, M. Tofte and R. Harper: The Definition of Standard ML. MIT Press (1990).
M.P. Nivela and F. Orejas: Initial behaviour semantics for algebraic specifications. in: D. Sannella (ed.): Selected Papers of the 5th Workshop on Specification of Abstract Data Types, Gullane, Scotland. LNCS 332, 184–207 (1988).
Z. Qian: Higher-order order-sorted algebra. Proc. Algebraic and Logic Programming, Nancy. LNCS 463, 86–100 (1990)
C. Reade: Elements of Functional Programming. Addison-Wesley (1989).
H. Reichel: Behavioural equivalence: a unifying concept for initial and final specification methods. Proc. 3rd Hungarian Computer Science Conf., Budapest, 27–39 (1981).
H. Reichel: a sketch approach to SPECTRAL semantics. Talk given at Informatik Kolloqium, Universität Bremen (1990).
J. Reynolds: Types, abstraction and parametric polymorphism. Information Processing '83, 513–523. North-Holland (1983).
D. Sannella: Formal program development in Extended ML for the working programmer. Proc. 3rd BCS/FACS Workshop on Refinement, Hursley Park. LNCS, to appear (1990).
D. Sannella and R. Burstall: Structured theories in LCF. Proc. 8th Colloq. on Trees in Algebra and Programming, L'Aquila, Italy. LNCS 159, 377–391 (1983).
O. Schoett: Data Abstraction and the Correctness of Modular Programming. Ph.D. thesis CST-42-87, Univ. of Edinburgh (1987).
D. Sannella, S. Sokolowski and A. Tarlecki: Toward formal development of programs from algebraic specifications: parameterisation revisited. Report 6/90, Univ. of Bremen (1990).
D. Sannella and A. Tarlecki: Program specification and development in Standard ML. Proc. 12th ACM Symp. on Principles of Programming Languages, New Orleans, 67–77 (1985).
D. Sannella and A. Tarlecki: Extended ML: an institution-independent framework for formal program development. Proc. Workshop on Category Theory and Computer Programming, Guilford. LNCS 240, 364–389 (1986).
D. Sannella and A. Tarlecki: On observational equivalence and algebraic specification. J. Comp. and Sys. Sciences 34, 150–178 (1987).
D. Sannella and A. Tarlecki: Toward formal development of programs from algebraic specifications: implementations revisited. Acta Informatica 25, 233–281 (1988).
D. Sannella and A. Tarlecki: Toward formal development of ML programs: foundations and methodology. Proc. Joint Conf. on Theory and Practice of Software Development, Barcelona. LNCS 352, 375–389 (1989).
D. Sannella and A. Tarlecki: A kernel specification formalism with higher-order parameterisation. Proc. 7th Workshop on Specification of Abstract Data Types, Wusterhausen. LNCS, to appear (1991).
D. Sannella and A. Tarlecki: Extended ML: past, present and future. Proc. 7th Workshop on Specification of Abstract Data Types, Wusterhausen. LNCS, to appear (1991).
D. Sannella and M. Wirsing: A kernel language for algebraic specification and implementation. Proc. Intl. Conf. on Foundations of Computation Theory, Borgholm, Sweden. LNCS 158, 413–427 (1983).
Å. Wikström: Functional Programming Using Standard ML. Prentice-Hall (1987).
M. Wirsing: Algebraic description of reusable software components. in: P. Wodon, E. Milgrom (eds.): COMPEURO 88, System Design: Concepts, Methods and Tools. IEE Comp. Soc. Press 834, 300–313 (1988).
M. Wirsing, R. Breu, R. Hennicker: Reusable specification components. in: M. Chytil (ed.): MFCS 88, Symp. on Mathematical Foundations of Computer Science, Karlsbad Aug. 88. LNCS 324, 121–137 (1988).
M. Wirsing, R. Hennicker, R. Stabl: MENUE — an example for the systematic reuse of specifications. in: C. Ghezzi, J. A. McDermid (eds.): ESEC 89, 2nd European Software Engineering Conf., Warwick 89. LNCS 387, 20–41 (1989).
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Krieg-Brückner, B., Sannella, D. (1991). Structuring specifications in-the-large and in-the-small: Higher-order functions, dependent types and inheritance in SPECTRAL. In: Abramsky, S., Maibaum, T.S.E. (eds) TAPSOFT '91. TAPSOFT 1991. Lecture Notes in Computer Science, vol 494. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3540539816_74
Download citation
DOI: https://doi.org/10.1007/3540539816_74
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-53981-0
Online ISBN: 978-3-540-46499-0
eBook Packages: Springer Book Archive