Swinging types=functions+relations+transition systems
type: Item
instance of: scholarly article
title: Swinging types=functions+relations+transition systems
zbMATH Open document ID: 0947.68098
DOI: 10.1016/S0304-3975(00)00171-7
published in: Theoretical Computer Science
publication date: 2000-08-21T00:00:00Z
review text: Swinging types provide an integrated framework for specifying software on the basis of many-sorted logic in terms of ``static'' functions and relations as well as ``dynamic'' transition systems. Swinging types combine equational, Horn and modal logic for the purpose of using evaluation and proof rules from all three logics for rapid prototyping and verification. A swinging specification separates from each other visible sorts that denote domains of data identified by their structure; hidden sorts that denote domains of data identified by their behavior in response to observers; \(\mu\)-predicates, i.e., least relations representing inductive(ly provable) properties of a system; and \(\nu\)-predicates, i.e., greatest relations representing complementary ``coinductive'' properties, which often describe behavioral aspects ``in the infinity''. Programming paradigms, such as functional, relational or state-oriented ones, and specification formalisms, such as algebraic, set-theoretic, rule-based, net-based, coalgebraic, order-theoretic ones, usually handle either static or dynamic components, either structural or behavioral aspects of a system. Swinging types admit the integrated design and analysis of these components and aspects. An integrated model is obtained naturally if all entities (objects, states, etc.) of the system are presented as terms built up of constructors for visible or hidden sorts, functions are specified in terms of conditional equations (=functional programs), least relations in terms of Horn clauses (=logic programs or transition system specifications) and greatest relations in terms of co-Horn clauses. Data equalities are either structural or behavioral, the former being least, the latter being greatest solutions of axioms that are determined by (components of) the type's signature. This paper mainly presents the theoretical foundations of swinging types, such as standard (term) models, criteria for structural and behavioral consistency, and proof …
Mathematics Subject Classification ID: 68Q85
zbMATH DE Number: 1493433
zbMATH Keywords: swinging types
zbMATH Keywords: transition systems
author: Peter Padawitz
describes a project that uses: CASL
describes a project that uses: CafeOBJ
describes a project that uses: EXPANDER
MaRDI profile type: Publication
cites work: Parametrized data types do not need highly constrained parameters
cites work: Q4702603
cites work: Observational structures and their logic
cites work: Q3365224
cites work: Q3993363
cites work: Process Algebra
cites work: Q4068686
cites work: Q4717366
cites work: Q5570212
cites work: Q3122692
cites work: Logic of transition systems
cites work: Proving the correctness of behavioural implementations
cites work: Behavioural and abstractor specifications
cites work: Partial abstract types
cites work: Q4256315
cites work: Specification of abstract dynamic-data types: A temporal logic approach
cites work: CafeOBJ Report. The language, proof techniques, and methodologies for object-oriented algebraicspecification
cites work: Algebraic implementation of abstract data types
cites work: Q3221381
cites work: Q4299864
cites work: Q4385542
cites work: Q4105777
cites work: Q4942101
cites work: An Oxford survey of order sorted algebra
cites work: Hidden coinduction: behavioural correctness proofs for objects
cites work: Structured operational semantics and bisimulation as a congruence
cites work: Abstract data types and software validation
cites work: Codatatypes in ML
cites work: Algebraic laws for nondeterminism and concurrency
cites work: Proof of correctness of data representations
cites work: Q4355684
cites work: Completion of a Set of Rules Modulo a Set of Equations
cites work: Conditional equational specifications of data types with partial operations for inductive theorem proving
cites work: Q3792217
cites work: Fixed point theorems and semantics: A folk tale
cites work: Q3839051
cites work: Q3687683
cites work: Q3809236
cites work: Notions of computation and monads
cites work: Semantics-Based Translation Methods for Modal Logics
cites work: Q4040341
cites work: Deduction and Declarative Programming
cites work: Inductive theorem proving for design specifications
cites work: Q4702600
cites work: Q5624635
cites work: Q5678447
cites work: Q3657409
cites work: An approach to object semantics based on terminal co-algebras
cites work: Universal coalgebra: A theory of systems
cites work: Toward formal development of programs from algebraic specifications: Implementations revisited
cites work: Automated deduction by theory resolution
cites work: Q4023900
cites work: Q4218096
cites work: Final algebra semantics and data type extensions
cites work: Specifications, models, and implementations of data abstractions
cites work: Q4385539
description: scientific article; zbMATH DE number 1493433