skip to main content
Idioma:

INSTITUTIONS - ABSTRACT MODEL-THEORY FOR SPECIFICATION AND PROGRAMMING

GOGUEN, JA ; BURSTALL, RM

Journal of the ACM, 1992-01, Vol.39 (1), p.95-146 [Periódico revisado por pares]

NEW YORK: Assoc Computing Machinery

Texto completo disponível

Citações Citado por
  • Título:
    INSTITUTIONS - ABSTRACT MODEL-THEORY FOR SPECIFICATION AND PROGRAMMING
  • Autor: GOGUEN, JA ; BURSTALL, RM
  • Assuntos: Applied sciences ; Computer programming ; Computer Science ; Computer Science, Hardware & Architecture ; Computer Science, Information Systems ; Computer Science, Software Engineering ; Computer Science, Theory & Methods ; Computer science; control theory; systems ; Dynamical systems ; Dynamics ; Exact sciences and technology ; Functions ; Language theory and syntactical analysis ; Logic ; Mathematical models ; Programming languages ; Science & Technology ; Semantics ; Sentences ; Signatures ; Specifications ; Studies ; Technology ; Theorem proving ; Theoretical computing ; Theory
  • É parte de: Journal of the ACM, 1992-01, Vol.39 (1), p.95-146
  • Notas: ObjectType-Article-1
    SourceType-Scholarly Journals-1
    ObjectType-Feature-2
    content type line 23
    ObjectType-Article-2
    ObjectType-Feature-1
  • Descrição: There is a population explosion among the logical systems used in computing science. Examples include first-order logic, equational logic, Horn-clause logic, higher-order logic, infinitary logic, dynamic logic, intuitionistic logic, order-sorted logic, and temporal logic; moreover, there is a tendency for each theorem prover to have its own idiosyncratic logical system. The concept of institution is introduced to formalize the informal notion of "logical system." The major requirement is that there is a satisfaction relation between models and sentences that is consistent under change of notation. Institutions enable abstracting away from syntactic and semantic detail when working on language structure "in-the-large"; for example, we can define language features for building large structures from smaller ones, possibly involving parameters, without commitment to any particular logical system. This applies to both specification languages and programming languages. Institutions also have applications to such areas as database theory and the semantics of artificial and natural languages. A first main result of this paper says that any institution such that signatures (which define notation) can be glued together, also allows gluing together theories (which are just collections of sentences over a fixed signature). A second main result considers when theory structuring is preserved by institution morphisms. A third main result gives conditions under which it is sound to use a theorem prover for one institution on theories from another. A fourth main result shows how to extend institutions so that their theories may include, in addition to the original sentences, various kinds of constraint that are. useful for defining abstract data types, including both "data" and "hierarchy" constraints. Further results show how to define institutions that allow sentences and constraints from two or more institutions. All our general results apply to such "duplex" and "multiplex" institutions.
  • Editor: NEW YORK: Assoc Computing Machinery
  • Idioma: Inglês
Links
Voltar para lista de resultados

  • Realização: ABCD-USP USP   Logos de Redes Sociais: Freepik

Buscando em bases de dados remotas. Favor aguardar.