Correctness of fixpoint transformations

DOI10.1016/0304-3975(94)90083-3MaRDI QIDQ1329743zbMATH OpenOpenAlexFDO

Authors Jiawang Wei

Publication date 3 April 1995

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0304-3975(94)90083-3

zbMATH Keywords

complete partial orderedcorrectness of fixed-point transformationsgeneral transformations of equations

Mathematics Subject Classification ID

Partial orders, general (06A06) Applications of universal algebra in computer science (08A70) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Review text

The paper deals with ``general transformations of equations, being not concerned with particular utilization of ``many-sorted equational logics in theoretical computer science: ``Transformations on a system of equations may change the solution set; those that preserve the desired solutions are called correct transformations. The objective of this paper is to study the correctness of fixed-point transformations in a general setting. The framework of complete partially ordered sets underlines the presentation. Even if this presentation is very general and appealing (including the use of ordinals and the beauty of the examples), we think that its (declared) main goal (``the results of this paper can be applied to various problems?!) was not satisfactorily pointed out.

Recommendations

• scientific article; zbMATH DE number 719843
• scientific article; zbMATH DE number 1089087
• The change of correctness under the transformation of equations
• scientific article; zbMATH DE number 1534593
• The equational logic of fixed points

Cites work

• A lattice-theoretical fixpoint theorem and its applications
• Chain-complete posets and directed sets with applications
• Constructive versions of Tarski's fixed point theorems
• Convergence of chaotic iterative least fixed point computations
• Equational languages
• Equivalences and transformations of regular systems - applications to recursive program schemes and grammars
• Global Data Flow Analysis and Iterative Algorithms
• scientific article; zbMATH DE number 4049098 (Why is no real title available?)
• scientific article; zbMATH DE number 3707731 (Why is no real title available?)
• scientific article; zbMATH DE number 3602653 (Why is no real title available?)
• scientific article; zbMATH DE number 3632470 (Why is no real title available?)
• scientific article; zbMATH DE number 1142319 (Why is no real title available?)
• scientific article; zbMATH DE number 1142327 (Why is no real title available?)
• scientific article; zbMATH DE number 3073037 (Why is no real title available?)
• Program derivation by fixed point computation
• Reasoning algebraically about recursion
• The convergence of functions to fixedpoints of recursive definitions
• Two Families of Languages Related to ALGOL

Cited in

(2)

• Correctness of transformations on register transfers
• The change of correctness under the transformation of equations

Describes a project that uses

Uses Software

• ALGOL 60

This page was built for publication: Correctness of fixpoint transformations

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1329743)