An informal approach to formal specifications

ABSTRACT

An attempt is made to help bridging the gap between theoretical research and the real practice of data base specification. Some fundamental problems that must be addressed are described and a number of formalisms that propose to attack them are overviewed. The case pro and against the use of formal specifications is presented.

REFERENCES

• 1: {As} M. M. Astrahan et al - "A history and evaluation of System R" - Research report RJ2843(36129), IBM S. Jose (1980).
• 2: A. Bolour , T. L. Anderson , L. J. Dekeyser , H. K. T. Wong, The role of time in information processing: a survey, ACM SIGMOD Record, v.12 n.3, p.27-50, April 1982 [doi>10.1145/984505.984508]
• 3: {BG} R. W. Burstall and J. Goguen - "Putting theories together to make specifications"-Proc. Fifth International Joint Conference on Artificial Intelligence (1977) 1045--1058.
• 4: {BGW} R. M. Balzer, N. M. Goldman and D. S. Wile - "Operational specification for rapid prototyping" - Technical Report, Information Sciences Institute, USC (1981).
• 5: Dines Bjørner , Hans Henrik Løvengreen, Formalization of Database Systems - and a Formal Definition of IMS (Invited Paper), Proceedings of the 8th International Conference on Very Large Data Bases, p.334-347, September 08-10, 1982
• 6: {BP} W. Bartussek and D. Parnas - "Using traces to write abstract specifications for software modules" - UNC Report 77-012 - University of North Carolina at Chapel Hill (1977).
• 7: {Brod} M. L. Brodie - "Type specification and databases" - topic outline for a panel in 8th International Conference on Very Large Data Bases (1982).
• 8: Frederick P. Brooks, Jr., The Mythical Man-Month: Essays on Softw, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1978
• 9: Michael L. Brodie , Joachim W. Schmidt, Final report of the ANSI/X3/SPARC DBS-SG relational database task group, ACM SIGMOD Record, v.12 n.4, p.1-62, July 1982 [doi>10.1145/984555.1108830]
• 10: {BZ} M. L. Brodie and S. N. Zilles (eds.) - Proc. of the Workshop on Data Abstraction, Databases and Conceptual Modelling - SIGMOD Record, 11, 2 (1981).
• 11: Marco R. Casanova , Phillip A. Bernstein, A Formal System for Reasoning about Programs Accessing a Relational Database, ACM Transactions on Programming Languages and Systems (TOPLAS), v.2 n.3, p.386-414, July 1980 [doi>10.1145/357103.357111]
• 12: {CCF} M. A. Casanova, J. M. V. de Castilho and A. L. Furtado - "Properties of conceptual and external schemas" - Proc. Formalization of Programming Concepts - North-Holland (1982) to appear.
• 13: {CF} M. A. Casanova and A. L. Furtado - "A family of temporal languages for the description of transition constraints" - Proc. Workshop on Logical Bases for Databases (1982) to appear.
• 14: Peter Pin-Shan Chen, The entity-relationship model—toward a unified view of data, ACM Transactions on Database Systems (TODS), v.1 n.1, p.9-36, March 1976 [doi>10.1145/320434.320440]
• 15: {CPLM} R. L. Carvalho, A. Pereda B., C. J. P. Lucena and T. S. E. Maibaum - "Data specification methods" - Proc. International Conference on Systems Methodology, Washington (1982).
• 16: C.J. J. Date, An Introduction to Database Systems, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1981
• 17: Edsger W. Dijkstra, How do we tell truths that might hurt?, ACM SIGPLAN Notices, v.17 n.5, p.13-15, May 1982 [doi>10.1145/947923.947924]
• 18: Walter Dosch , Gianfranco Mascari , Martin Wirsing, On the Algebraic Specification of Databases, Proceedings of the 8th International Conference on Very Large Data Bases, p.370-385, September 08-10, 1982
• 19: James Edward Donahue, Complementary Definitions of Programming Language Semantics, Springer-Verlag New York, Inc., Secaucus, NJ, 1976
• 20: {EK} H. Ehrig and H. J. Kreowski - "Applications of graph grammar theory to consistency, synchronization and scheduling in data base systems" - Information Systems, vol. 5 (1980) 225--238.
• 21: {EKW} H. Ehrig, H. J. Kreowski and H. Weber - "Algebraic specification schemes for data base systems" - Proc. 4th International Conference on Very Large Data Bases (1978) 427--440.
• 22: Nicholas V. Findler, Associative Networks: The Representation and Use of Knowledge by Computers, Academic Press, Inc., Orlando, FL, 1979
• 23: Antonio L. Furtado, Transformations of Data Base Structures, Proceedings of the International Workshop on Graph-Grammars and Their Application to Computer Science and Biology, p.224-236, October 30-November 03, 1978
• 24: {Fu2} A. L. Furtado - "A W-grammar approach to data bases" - Monograph 9/82, PUC/RJ (1982).
• 25: A. L. Furtado , P. A. S. Veloso, Procedural specifications and implementations for abstract data types, ACM SIGPLAN Notices, v.16 n.3, p.53-62, March 1981 [doi>10.1145/947825.947828]
• 26: Antonio L. Furtado , Paulo A. S. Veloso, Specification of data bases through rewriting rules, Proceedings of the 2nd International Workshop on Graph-Grammars and Their Application to Computer Science, p.102-114, October 04-08, 1982
• 27: Antonio L. Furtado , Paulo A. S. Veloso , José Mauro V. de Castilho, Verification and Testing of S-ER Representations, Proceedings of the Second International Conference on the Entity-Relationship Approach to Information Modeling and Analysis, p.123-147, October 12-14, 1981
• 28: {Ga} H. Gallaire - "Impacts of logic on data bases" - Proc. 7th International Conference on Very Large Data Bases (1981) 248--259.
• 29: {Ge} S. L. Gerhart et al - "An overview of Affirm: a specification and verification system" - Proc. IFIP (1980) 343--348.
• 30: John Guttag , J. J. Horning, Formal specification as a design tool, Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.251-261, January 28-30, 1980, Las Vegas, Nevada [doi>10.1145/567446.567471]
• 31: {GHM} J. Guttag, E. Horowitz and D. R. Musser - "The design of data type specifications" in 'Current trends in programming methodologies' - R. T. Yeh (ed.) vol. IV - Prentice-Hall (1978).
• 32: Herve Gallaire , Jack Minker, Logic and Data Bases, Perseus Publishing, 1978
• 33: Herve Gallaire , Jack Minker , Jean M. Nicholas, Advances in Data Base Theory, Perseus Publishing, 1981
• 34: {Go} C. C. Gotlieb - "Some large questions about very large data bases" - Proc. Sixth Very Large Data Bases Conference - (1980) 3--7.
• 35: {Gr} J. J. van Griethuysen (ed.) - Concepts and terminology for the conceptual schema and the information base" - report from the ISO TC97/SC5/WG3 group (1982).
• 36: {GT} J. A. Goguen and J. J. Tardo - "An introduction to OBJ: a language for writing and testing formal algebraic specifications" - Proc. Specifications of Reliable Software - IEEE Computer Society (1979).
• 37: {GTW} J. A. Goguen, J. W. Thatcher and E. G. Wagner - "An initial algebra approach to the specification, correctness and implementation of abstract data types" - in 'Current trends in programming methodology' - R. T. Yeh (ed.) - vol IV - Prentice-Hall (1978) 80--149.
• 38: {HL} C. A. R. Hoare and P. E. Lauer - "Consistent and complementary formal theories of the semantics of programming languages" - Acta Informatica 3 (1974) 135--153.
• 39: C.A. R. Hoare, Data reliability, Proceedings of the international conference on Reliable software, p.528-533, April 21-23, 1975, Los Angeles, California
• 40: {Hol} J. B. Holton - "Are the new programming techniques being used?" - Datamation - July (1977) 97--103.
• 41: Barry E. Jacobs, On Database Logic, Journal of the ACM (JACM), v.29 n.2, p.310-332, April 1982 [doi>10.1145/322307.322310]
• 42: Witold Lipski, Jr., On Databases with Incomplete Information, Journal of the ACM (JACM), v.28 n.1, p.41-70, Jan. 1981 [doi>10.1145/322234.322239]
• 43: Peter C. Lockemann , Heinrich C. Mayr , Wolfgang H. Weil , Wolfgang H. Wohlleber, Data abstractions for database systems, ACM Transactions on Database Systems (TODS), v.4 n.1, p.60-75, March 1979 [doi>10.1145/320064.320067]
• 44: {LZ} B. Liskov and S. Zilles - "An introduction to formal specifications of data abstractions" in 'Current trends in programming methodologies' - R. T. Yeh (ed.) - vol I - Prentice-Hall (1977) 1--32.
• 45: {Mink} J. Minker - "On indefinite databases and the closed world assumption" - Technical Report 1076, University of Maryland (1981).
• 46: {Mins} M. Minsky - "A framework for representing knowledge" - in 'The psychology of computer vision' - P. H. Winston (ed.) - McGraw-Hill (1975) 413--424.
• 47: Shamkant B. Navathe , Suresh G. Gadgil, A Methodology for View Inegration in Logical Database Design, Proceedings of the 8th International Conference on Very Large Data Bases, p.142-164, September 08-10, 1982
• 48: {NO} E. J. Neuhold and T. Olnhoff - "The Vienna Definition Method (VDM) and its use for the specification of a relational data base system" - in 'Information Processing 80' - S. Lavington (ed.) - North-Holland (1980).
• 49: {Pag} F. G. Pagan - "Formal specification of programming languages" - Prentice-Hall (1981).
• 50: {Pao} P. Paolini - "Verification of views and application programs" - Proc. Workshop on Formal Bases for Databases, Toulouse (1979).
• 51: {Par} D. L. Parnas - "The use of precise specifications in the development of software"-in 'Information Processing 77' - B. Gilchrist (ed.) - North-Holland (1977) 861--867.
• 52: {RB} D. Ridjanovic and M. L. Brodie - "Defining database dynamics with attribute grammars" - Information Processing Letters, vol. 14, n. 3 (1982) 132--138.
• 53: {Rou} N. Roussopoulos - "CSDL: a conceptual schema definition language for the design of data base applications" - IEEE Trans. on Software Engineering, SE-5,5 (1979) 481--496.
• 54: Lawrence A. Rowe, Data abstraction from a programming language viewpoint, Proceedings of the 1980 workshop on Data abstraction, databases and conceptual modeling, p.29-35, June 23-26, 1980, Pingree Park, Colorado, United States
• 55: Daniel Schwabe, Formal techniques for the specification and verification of protocols, 1981
• 56: {Sco} D. Scott - "Outline of a mathematical theory of computation" - Proc. Fourth Annual Princeton Conference on Information Sciences and Systems (1970) 169--176.
• 57: {Sh} M. Shaw - "The impact of abstraction concerns on modern programming languages" - Proc. of the IEEE, 68, 9 (1980) 1119--1130.
• 58: E. H. Sibley, Database management systems past and present, Proceedings of the 1980 workshop on Data abstraction, databases and conceptual modeling, p.192, June 23-26, 1980, Pingree Park, Colorado, United States
• 59: Ulrich Schiel , Antonio L. Furtado , Erich J. Neuhold , Marco A. Casanova, Towards multi-level and modular conceptual schema specifications, Information Systems, v.9 n.1, p.43-57, 1984 [doi>10.1016/0306-4379(84)90015-2]
• 60: {SMF} C. S. dos Santos, T. S. E. Maibaum and A. L. Furtado - "Conceptual modelling of data base operations" - International Journal of Computer and Information Sciences, 10, 5 (1981) 299--314.
• 61: John Miles Smith , Diane C. P. Smith, Database abstractions: aggregation and generalization, ACM Transactions on Database Systems (TODS), v.2 n.2, p.105-133, June 1977 [doi>10.1145/320544.320546]
• 62: {Su} B. Sundgren - "A conceptual foundation for the infological approach to data bases" - in 'Data base management' - J. W. Klimbie and K. L. Koffeman (eds.) - North-Holland (1974) 61--94.
• 63: R. D. Tennent, The denotational semantics of programming languages, Communications of the ACM, v.19 n.8, p.437-453, Aug. 1976 [doi>10.1145/360303.360308]
• 64: Toby J. Teorey , James P. Fry, Design of Database Structures, Prentice Hall Professional Technical Reference, 1982
• 65: {TK} D. C. Tsichritzis and A. Klug (eds.) - "The ANSI/X3/SPARC DBMS framework - report of the study group" - AFIPS Press (1977).
• 66: Dionysios C. Tsichritzis , Frederick H. Lochovsky, Data Models, Prentice Hall Professional Technical Reference, 1982
• 67: {VCF} P. A. S. Veloso, J. M. V. de Castilho and A. L. Furtado - "Systematic derivation of complementary specifications" - Proc. Seventh International Conference on Very Large Data Bases (1981) 409--421.
• 68: {VF} P. A. S. Veloso and A. L. Furtado - "Multilevel specifications based on traces" - Proc. International Computer Symposium on Application Systems Development, Nurnberg (1983, to appear).
• 69: {Wi} A. van Wijngaarden et al (eds.) - "Revised report on the algorithmic language ALGOL 68" - Acta Informatica, 5 (1975) 1--236.
• 70: David H D Warren , Luis M. Pereira , Fernando Pereira, Prolog - the language and its implementation compared with Lisp, Proceedings of the 1977 symposium on Artificial intelligence and programming languages, p.109-115, August 15-17, 1977
• 71: Stephen N. Zilles, Types, algebras and modeling, Proceedings of the 1980 workshop on Data abstraction, databases and conceptual modeling, p.207-209, June 23-26, 1980, Pingree Park, Colorado, United States

INDEX TERMS

Keywords:
abstract data types, data bases, data models, denotational methods, formal specifications, grammars, integrity constraints, logic