Skip to main content
SpringerLink
Log in

Theory of Computation and Specification over Abstract Data Types, and its Applications

  • Conference paper
Logic, Algebra, and Computation

Part of the book series: NATO ASI Series ((NATO ASI F,volume 79))

Abstract

The theory of computable functions on abstract data types is outlined. The problems of extending the theory to establish the scope and limits of the specification and verification of functions are described. Applications of this general mathematical theory to hardware design, program verification and logic programming are discussed.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  • J W de Bakker, Mathematical theory of program correctness, Prentice Hall, 1980.

    MATH  Google Scholar 

  • J A Bergstra, J Tiuryn and J V Tucker, Floyd’s principle, correctness theories and program equivalents, Theoretical Computer Science, 17 (1982) 451–476.

    MathSciNet  Google Scholar 

  • J A Bergstra and J V Tucker, A characterisation of computable data types by means of a finite equational specification method, in J W de Bakker and J van Leeuwen (eds.) Automata, Languages and Programming, Seventh Colloquium, Noordwijkerhout, 1980, Springer Lecture Notes in Computer Science 81, Springer-Verlag, Berlin, 1980, pp. 76–90.

    Google Scholar 

  • J A Bergstra and J V Tucker, Algebraic specifications of computable and semi-computable data structures, Research Report IW 121, Mathematisch Centrum, 1980.

    Google Scholar 

  • J A Bergstra and J V Tucker, Algebraic specifications of computable and semi-computable data types, Theoretical Computer Science, 50 (1987) 137–181.

    Article  MATH  MathSciNet  Google Scholar 

  • J A Bergstra and J V Tucker, Initial and final algebra semantics for data type specifications: two characterisation theorems, Society for Industrial and Applied Mathematics (SIAM) J on Computing, 12 (1983) 366–387.

    MATH  MathSciNet  Google Scholar 

  • A G Cohn, A more expressive formulation of many sorted logic, J. Automated Reasoning 3 (1987) 113–200.

    Article  MATH  Google Scholar 

  • J Derrick, G Lajos and J V Tucker, Specification and verification of synchronous concurrent algorithms using the Nuprl proof development system, Centre for Theoretical Computer Science Report, University of Leeds, in preparation.

    Google Scholar 

  • J Derrick and J V Tucker, Logic programming and abstract data types, in Proceedings of 1988 UK IT Conference, held under the auspices of the Information Engineering Directorate of the Department of Trade and Industry (DTI), Institute of Electrical Engineers (IEE), 1988, pp. 217–219.

    Google Scholar 

  • H Ehrig and B Mahr, Fundamentals of algebraic specifications 1 — Equations and initial semantics, Springer-Verlag, 1985.

    Google Scholar 

  • S M Eker, Foundations for the design of rasterisation algorithms and architectures, PhD thesis, University of Leeds, in preparation.

    Google Scholar 

  • S M Eker, V Stavridou and J V Tucker, Verification of synchronous concurrent algorithms using OBJ3. A case study of the Pixel Planes architecture, in Proceedings of Workshop on Designing Correct Circuits, Oxford, 1990, in preparation.

    Google Scholar 

  • S M Eker and J V Tucker, Specification, derivation and verification of concurrent line drawing algorithms and architectures, in R A Earnshaw (ed.), Theoretical foundations of computer graphics and CAD, Springer-Verlag, 1988, pp. 449–516.

    Chapter  Google Scholar 

  • S M Eker and J V Tucker, Specification and verification of synchronous concurrent algorithms: a case study of the Pixel Planes architecture, in P M Dew, R A Earnshaw and T R Heywood (eds), Parallel processing for computer vision and display, Addison Wesley, 1989, pp.16–49.

    Google Scholar 

  • J E Fenstad, General recursion theory: An axiomatic approach, Springer-Verlag, Berlin, 1980.

    MATH  Google Scholar 

  • M Fitting, Fundamentals of generalised recursion theory, North-Holland, Amsterdam, 1981.

    Google Scholar 

  • F Fogelman Soulie, Y Robert, M Tchuente (eds.), Automata networks in computer science, Manchester University Press, 1986.

    Google Scholar 

  • J A Goguen, J W Thatcher, E G Wagner, and J B Wright, An initial algebra approach to the specification, correctness and implementation of abstract data types, in R T Yeh (ed.), Current trends in programming methodology: IV Data structuring, Prentice Hall, 1978, pp. 80–149.

    Google Scholar 

  • J A Goguen and J Meseguer, Equality, types, modules, and (why not?) generics for logic programming, J Logic Programming, 2 (1984) 179–210.

    Article  MathSciNet  Google Scholar 

  • J A Goguen and J Meseguer, Unifying functional, object-oriented and relational programming with logical semantics, Report SRI-CSL-87–7, SRI International, 1987.

    Google Scholar 

  • S Greibach, Theory of program structures: schemes, semantics, verification, Springer Lecture Notes in Computer Science 36, Berlin, 1975.

    Book  MATH  Google Scholar 

  • N A Harman and J V Tucker, Clocks, retimings, and the formal specification of a UART, in G Milne (ed.) The fusion of hardware design and verification (Proceedings of IFIP Working Group 10.2 Working Conference), North-Holland, 1988, pp. 375–396.

    Google Scholar 

  • N A Harman and J V Tucker, The formal specification of a digital correlator I: User specification process, Centre for Theoretical Computer Science, Report 9.87, University of Leeds, 1987. Also in K McEvoy and J V Tucker [90].

    Google Scholar 

  • N A Harman and J V Tucker, Formal specifications and the design of verifiable computers, in Proceedings of 1988 UK IT Conference, held under the auspices of the Information Engineering Directorate of the Department of Trade and Industry (DTI), Institute of Electrical Engineers (IEE), 1988, pp. 500–503.

    Google Scholar 

  • L A Harrington et al. (eds.) Harvey Friedman’s research on the foundations of Mathematics, North-Holland, 1985.

    MATH  Google Scholar 

  • K M Hobley, The specification and verification of synchronous concurrent algorithms, PhD thesis, University of Leeds, in preparation.

    Google Scholar 

  • K M Hobley, B C Thompson, and J V Tucker, Specification and verification of synchronous concurrent algorithms: a case study of a convolution algorithm, in G Milne (ed.) The fusion of hardware design and verification (Proceedings of IFIP Working Group 10.2 Working Conference), North-Holland, 1988, pp. 347–374.

    Google Scholar 

  • K Hobley and J V Tucker, Clocks and retimings, in preparation.

    Google Scholar 

  • A V Holden, J V Tucker and B C Thompson, The computational structure of neural systems, in A V Holden and V I Kryukov (eds.) Neurocomputers and attention. I: Neurobiology, synchronisation and chaos, Manchester University Press, 1990.

    Google Scholar 

  • A V Holden, J V Tucker and B C Thompson, Can excitable media be considered as computational systems? in A V Holden, M Markus, H G Othmer (eds.) Nonlinear wave processes in excitable media, Plenum, New York, 1990, pp. 509–516.

    Google Scholar 

  • A J Kfoury, The pebble game and logics of programs, in Harrington et al. [1985], pp. 317–329.

    Google Scholar 

  • J W Lloyd, Foundations of logic programming, Springer-Verlag, 1984.

    MATH  Google Scholar 

  • A I Mal’cev, Algebraic systems, Springer-Verlag, 1973.

    MATH  Google Scholar 

  • A I Mal’cev, The metamathematics of algebraic systems: Collected Papers 1936–1967, North-Holland, 1971.

    Google Scholar 

  • A R Martin and J V Tucker, The concurrent assignment representation of synchronous systems, in J W de Bakker, A J Nijman and P C Treleaven (eds.), PARLE: Parallel Architectures and Languages Europe, Vol II Parallel languages, Springer Lecture Notes in Computer Science 259, Springer-Verlag, 1987, pp. 369–386.

    Google Scholar 

  • A R Martin and J V Tucker, A revised and expanded edition appears in Parallel Computing 9 (1988/89) 227–256.

    Google Scholar 

  • K McEvoy and J V Tucker (eds.), Theoretical foundations of VLSI design, Cambridge University Press, 1990

    MATH  Google Scholar 

  • K Meinke, A graph theoretic model of synchronous concurrent algorithms, PhD Thesis, School of Computer Studies, University of Leeds, Leeds, 1988.

    Google Scholar 

  • K Meinke, Universal algrebra in higher types, Theoretical Computer Science, to appear.

    Google Scholar 

  • K Meinke, Fixed point and initial algebra semantics of recursion equations, Computer Science Division Research Report, University College of Swansea, in preparation.

    Google Scholar 

  • K Meinke and J V Tucker, Specification and representation of synchronous concurrent algorithms, in F H Vogt (ed.) Concurrency ′88, Springer Lecture Notes in Computer Science 335, Springer-Verlag, 1988, pp.163–180.

    Google Scholar 

  • K Meinke and J V Tucker, Universal algebra in S Abramsky, D Gabbay, T S E Maibaum (eds.) Handbook of logic in computer science, OUP, to appear.

    Google Scholar 

  • J C Shepherdson, Algorithmic procedures, generalised Turing algorithms, and elementary recursion theory, in Harrington et al. [1985], pp. 285–308.

    Google Scholar 

  • H Simmons, The realm of primitive recursion, Archive Math. Logic, 27 (1988) 117–188.

    Article  MathSciNet  Google Scholar 

  • B C Thompson, A mathematical theory of synchronous concurrent algorithms. PhD Thesis, School of Computer Studies, University of Leeds, 1987.

    Google Scholar 

  • B C Thompson and J V Tucker, Theoretical considerations in algorithm design, in R A Earnshaw (ed.), Fundamental algorithms for computer graphics, Springer-Verlag, 1985, pp. 855–878.

    Chapter  Google Scholar 

  • B C Thompson and J V Tucker, A parallel deterministic language and its application to synchronous concurrent algorithms, in Proceedings of 1988 UK IT Conference, held under the auspices of the Information Engineering Directorate of the Department of Trade and Industry (DTI), Institute of Electrical Engineers (IEE), 1988, pp. 228–231.

    Google Scholar 

  • B C Thompson and J V Tucker, Synchronous concurrent algorithms, Computer Science Division Research Report, University College of Swansea, in preparation.

    Google Scholar 

  • J V Tucker and J I Zucker, Program correctness over abstract data types, with error state semantics, North Holland, 1988.

    MATH  Google Scholar 

  • J V Tucker and J I Zucker, Horn programs and semicomputable relations on abstract structures, Automata, Languages and Programming 1989, Proceedings of the Sixteenth Colloquium, Stresa, Springer Lecture Notes in Computer Science 372, Springer-Verlag, 1989, pp.745–760

    Google Scholar 

  • J V Tucker, S S Wainer and J I Zucker, Provably computable functions on abstract data types, Automata, Languages and Programming 1990, Proceedings of the Seventeenth Colloquium, Coventry, Springer Lecture Notes in Computer Science, Springer-Verlag, 1990.

    Google Scholar 

  • C Walther, A many sorted calculus based on resolution and paramodulation, Pitman, 1987.

    MATH  Google Scholar 

  • A Williams, Theoretical and empirical studies in VLSI complexity theory, PhD Thesis, School of Computer Studies, University of Leeds, Leeds, 1989.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Mathematics and Computer Science, University College of Swansea, Singleton Park, Swansea, SA2 8PP, Wales

    J. V. Tucker

Authors
  1. J. V. Tucker
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Technische Universität München, Postfach 202 420, W-8000, München, Federal Republic of Germany

    Friedrich L. Bauer (Professor Emeritus) (Professor Emeritus)

Rights and permissions

Reprints and permissions

Copyright information

© 1991 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Tucker, J.V. (1991). Theory of Computation and Specification over Abstract Data Types, and its Applications. In: Bauer, F.L. (eds) Logic, Algebra, and Computation. NATO ASI Series, vol 79. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-76799-9_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-76799-9_1

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-76801-9

  • Online ISBN: 978-3-642-76799-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation