AbstractThe use of subtyping is explored in the context of a style of constructive specification. The intention is to enhance expressiveness and strengthen syntactic controls. The resulting specification style is part of a wide spectrum language, ABEL, developed at the Oslo University. A concept of signature completeness is presented, as well as a completion algorithm. Some results relating to weak, strong, and optimal typing are proved.
Categories and Subject Descriptors: D.1.1 [Programming Techniques]: Applicative (Functional) Programming; D.2.1 [Software Engineering]: Requirements/Specifications; D.2.4 [Software Engineering]: Program Verification; D.3.3 [Programming Languages]: Language Constructs and Features; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs; F.3.3 [Logics and Meanings of Programs]: Studies of Program Constructs
Additional Key Words and Phrases: algebraic specification, specification language, generator induction, subtypes, partial functions, definedness, syntactic control
Selected papers that cite this one
- Gilles Barthe. Order-sorted inductive types. Information and Computation, 149(1):42-76, 25 February 1999.
- Bjørn Kristoffersen and Ole-Johan Dahl. On Introducing Higher Order Functions in ABEL. Nordic Journal of Computing, 5(1):50-69, Spring 1998.
Selected references
- Morten Elvang-Gøransson and Olaf Owe. A simple sequent calculus for partial functions. Theoretical Computer Science, 114(2):317-330, 21 June 1993. Note.
- Kokichi Futatsugi, Joseph A. Goguen, Jean-Pierre Jouannaud, and José Meseguer. Principles of OBJ2. In Conference Record of the Twelfth Annual ACM Symposium on Principles of Programming Languages, pages 52-66, New Orleans, Louisiana, January 1985.
- C. B. Jones and C. A. Middelburg. A typed logic of partial functions reconstructed classically. Acta Informatica, 31(5):399-430, 1994.
- Bjørn Kristoffersen and Ole-Johan Dahl. On Introducing Higher Order Functions in ABEL. Nordic Journal of Computing, 5(1):50-69, Spring 1998.
- Olaf Owe. Partial logics reconsidered: A conservative approach. Formal Aspects of Computing, 5(3):208-223, 1993.
- Olaf Owe and Ole-Johan Dahl. Generator induction in order sorted algebras. Formal Aspects of Computing, 3(1):2-20, 1991.