Choose an application

• Reference Manager
• EndNote
• RefWorks (Direct export to RefWorks)

This volume contains the proceedings of the conference on Fundamentals of Computation Theory held in Szeged, Hungary, August 21-25, 1989. The conference is the seventh in the series of the FCT conferences initiated in 1977 in Poznan-Kornik, Poland. The papers collected in this volume are the texts of invited contributions and shorter communications falling into one of the following sections: - Efficient Computation by Abstract Devices: Automata, Computability, Probabilistic Computations, Parallel and Distributed Computing; - Logics and Meanings of Programs: Algebraic and Categorical Approaches to Semantics, Computational Logic, Logic Programming, Verification, Program Transformations, Functional Programming; - Formal Languages: Rewriting Systems, Algebraic Language Theory; - Computational Complexity: Analysis and Complexity of Algorithms, Design of Efficient Algorithms, Algorithms and Data Structures, Computational Geometry, Complexity Classes and Hierarchies, Lower Bounds.

Computer science --- 681.3*D24 --- 681.3*E5 --- 681.3*F12 --- 681.3*I2 --- Program verification: assertion checkers; correctness proofs; reliability; validation (Software engineering)--See also {681.3*F31} --- Files: backup/recovery; optimization; organization/structure; sorting/searching (Data) --- Modes of computation: alternation and nondeterminism; parallelism; probabilistic computation; relations among modes; relativized computation --- Artificial intelligence. AI --- 681.3*E5 Files: backup/recovery; optimization; organization/structure; sorting/searching (Data) --- 681.3*D24 Program verification: assertion checkers; correctness proofs; reliability; validation (Software engineering)--See also {681.3*F31} --- 681.3*I2 Artificial intelligence. AI --- 681.3*F12 Modes of computation: alternation and nondeterminism; parallelism; probabilistic computation; relations among modes; relativized computation --- Computer science. --- Computer software. --- Logic design. --- Microprogramming. --- Combinatorics. --- Computation by Abstract Devices. --- Algorithm Analysis and Problem Complexity. --- Logics and Meanings of Programs. --- Mathematical Logic and Formal Languages. --- Control Structures and Microprogramming. --- Combinatorics --- Algebra --- Mathematical analysis --- Computer programming --- Design, Logic --- Design of logic systems --- Digital electronics --- Electronic circuit design --- Logic circuits --- Machine theory --- Switching theory --- Software, Computer --- Computer systems --- Informatics --- Science --- Informatique

Choose an application

• Reference Manager
• EndNote
• RefWorks (Direct export to RefWorks)

The hierarchical decomposition of programs into smaller ones is generally considered imperative to master the complexity of large programs. The impact of this principle of program decomposition on the specification and verification of parallel executed programs is the subject of this monograph. Two important yardsticks for verification methods, those of compositionality and modularity, are made precise. The problem of reusing software is addressed by the introduction of the notion of specification adaptation. Within this context, different methods for specifying the observable behavior with respect to partial correctness of communicating processes are considered, and in particular the contrast between the "programs are predicates" and the "programs are predicate transformers" paradigms is shown. The associated formal proof systems are proven sound and complete in various senses with respect to the denotational semantics of the programming language, and they are related to each other to give an in-depth comparison between the different styles of program verification. The programming language TNP used here is near to actual languages like Occam. It combines CCS/CSP style communication based programming with state based programming, and allows dynamically expanding and shrinking networks of processes.

Programming --- Automatic theorem proving --- Parallel processing (Electronic computers) --- 681.3*D21 --- 681.3*D24 --- 681.3*D31 --- 681.3*F31 --- Requirements/specifications: languages; methodologies; tools (Software engineering)--See also {681.3*D31} --- Program verification: assertion checkers; correctness proofs; reliability; validation (Software engineering)--See also {681.3*F31} --- Formal definitions and theory: semantics; syntax (Programming languages)--See also {681.3*D21}; {681.3*F31}; {681.3*F32}; {681.3*F42}; {681.3*F43} --- Specifying anf verifying and reasoning about programs: assertions; invariants; mechanical verification; pre- and post-conditions (Logics and meanings of programs)--See also {681.3*D21}; {681.3*D24}; {681.3*D31}; {681.3*E1} --- 681.3*F31 Specifying anf verifying and reasoning about programs: assertions; invariants; mechanical verification; pre- and post-conditions (Logics and meanings of programs)--See also {681.3*D21}; {681.3*D24}; {681.3*D31}; {681.3*E1} --- 681.3*D31 Formal definitions and theory: semantics; syntax (Programming languages)--See also {681.3*D21}; {681.3*F31}; {681.3*F32}; {681.3*F42}; {681.3*F43} --- 681.3*D24 Program verification: assertion checkers; correctness proofs; reliability; validation (Software engineering)--See also {681.3*F31} --- 681.3*D21 Requirements/specifications: languages; methodologies; tools (Software engineering)--See also {681.3*D31} --- Théorèmes --- Parallélisme (Informatique) --- Démonstration automatique --- Théorèmes --- Parallélisme (Informatique) --- Démonstration automatique --- Logic design. --- Software engineering. --- Computer science. --- Logics and Meanings of Programs. --- Software Engineering. --- Programming Languages, Compilers, Interpreters. --- Computer software engineering --- Engineering --- Informatics --- Science --- Design, Logic --- Design of logic systems --- Digital electronics --- Electronic circuit design --- Logic circuits --- Machine theory --- Switching theory --- Lncs --- Concurrency

Choose an application

• Reference Manager
• EndNote
• RefWorks (Direct export to RefWorks)

The present volume contains the proceedings of Logic at Botik '89, a symposium on logical foundations of computer science organized by the Program Systems Institute of the USSR Academy of Sciences and held at Pereslavl-Zalessky, USSR, July 3-8, 1989. The scope of the symposium was very broad; the topics of interest were: complexity of formal systems, constructive mathematics in computer science, denotational and operational semantics of programs, descriptive complexity, dynamic and algorithmic logics and schematology, formal tools to describe concurrent computations, lambda calculus and related topics, foundations of logic programming, logical foundations of database theory, logics for knowledge representation, modal and temporal logics, type theory in programming, and verification of programs. Thus, the papers in this volume represent many interesting trends in logical foundations of Computer Science, ranging from purely theoretical research to practical applications of theory.

Computer science --- 681.3*D24 --- 681.3*D31 --- 681.3*D33 --- 681.3*F3 --- 681.3*F41 --- Program verification: assertion checkers; correctness proofs; reliability; validation (Software engineering)--See also {681.3*F31} --- Formal definitions and theory: semantics; syntax (Programming languages)--See also {681.3*D21}; {681.3*F31}; {681.3*F32}; {681.3*F42}; {681.3*F43} --- Languages constructs: abstract data types; concurrent programming structures;control structures; coroutines (Programming languages) --- Logics and meanings of programs (Theory of computation) --- Mathematical logic: computability theory; computational logic; lambda calculus; logic programming; mechanical theorem proving; model theory; proof theory;recursive function theory--See also {681.3*F11}; {681.3*I22}; {681.3*I23} --- 681.3*F41 Mathematical logic: computability theory; computational logic; lambda calculus; logic programming; mechanical theorem proving; model theory; proof theory;recursive function theory--See also {681.3*F11}; {681.3*I22}; {681.3*I23} --- 681.3*F3 Logics and meanings of programs (Theory of computation) --- 681.3*D33 Languages constructs: abstract data types; concurrent programming structures;control structures; coroutines (Programming languages) --- 681.3*D31 Formal definitions and theory: semantics; syntax (Programming languages)--See also {681.3*D21}; {681.3*F31}; {681.3*F32}; {681.3*F42}; {681.3*F43} --- 681.3*D24 Program verification: assertion checkers; correctness proofs; reliability; validation (Software engineering)--See also {681.3*F31} --- Information theory. --- Logic design. --- Software engineering. --- Computer science. --- Artificial intelligence. --- Logic, Symbolic and mathematical. --- Theory of Computation. --- Logics and Meanings of Programs. --- Software Engineering. --- Mathematical Logic and Formal Languages. --- Artificial Intelligence. --- Mathematical Logic and Foundations. --- Algebra of logic --- Logic, Universal --- Mathematical logic --- Symbolic and mathematical logic --- Symbolic logic --- Mathematics --- Algebra, Abstract --- Metamathematics --- Set theory --- Syllogism --- AI (Artificial intelligence) --- Artificial thinking --- Electronic brains --- Intellectronics --- Intelligence, Artificial --- Intelligent machines --- Machine intelligence --- Thinking, Artificial --- Bionics --- Cognitive science --- Digital computer simulation --- Electronic data processing --- Logic machines --- Machine theory --- Self-organizing systems --- Simulation methods --- Fifth generation computers --- Neural computers --- Informatics --- Science --- Computer software engineering --- Engineering --- Design, Logic --- Design of logic systems --- Digital electronics --- Electronic circuit design --- Logic circuits --- Switching theory --- Communication theory --- Communication --- Cybernetics