A relational division operator: The conjugate kernel

DOI10.1016/0304-3975(93)90074-4MaRDI QIDQ2367540zbMATH OpenOpenAlexWikidataFDO

Authors Ali Jaoua, Noureddine Boudriga, Jules Desharnais, Fatma Mili, Ali Mili

Publication date 19 January 1994

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

Full work available at URL https://doi.org/10.1016/0304-3975(93)90074-4

zbMATH Keywords

axiomatic semanticsprogram constructionprogram correctnessrelation algebrarelational division operatorweakest preconditionweakest prespecification

Mathematics Subject Classification ID

Cylindric and polyadic algebras; relation algebras (03G15) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Discrete mathematics in relation to computer science (68R99)

Review text

A binary operator on relations, called conjugate kernel, is introduced. It is defined as a restriction of a residual and behaves as a kind of inverse of the relational product operator. It is shown how relational algebraic methods can be useful in describing fundamental concepts of programming. The conjugate kernel operator is related with Hoare's weakest pre- and postspecification, Joseph's weakest pre- and postspecification, and Dijkstra's weakest precondition. For example, it is proven that, if there exists a solution of the weakest prespecification problem, the conjugate kernel describes an optimal solution. Furthermore, the connection between the conjugate kernel operator and the notion of program correctness is discussed and the use of conjugate kernels in program construction is demonstrated. Finally, the results are compared with other studies of division-like operators for binary relations.

Recommendations

• Binary relations. Addenda. 1: Kernel, restrictions and inducing, relational morphisms
• On the mathematics of sequential decompositions
• scientific article; zbMATH DE number 3923469
• Conjugative relations and applications
• Division and renaming in relational algebras

Cites work

• A relational approach to the design of deterministic programs
• Heuristics for constructing while loops
• scientific article; zbMATH DE number 4020448 (Why is no real title available?)
• scientific article; zbMATH DE number 3740740 (Why is no real title available?)
• scientific article; zbMATH DE number 107838 (Why is no real title available?)
• scientific article; zbMATH DE number 194258 (Why is no real title available?)
• scientific article; zbMATH DE number 3204690 (Why is no real title available?)
• scientific article; zbMATH DE number 3378527 (Why is no real title available?)
• scientific article; zbMATH DE number 3070503 (Why is no real title available?)
• Programming as a Discipline of Mathematical Nature
• Programs as partial graphs. I: Flow equivalence and correctness
• Regularity of relations: A measure of uniformity
• Relational heuristics for the design of deterministic programs
• Relations binaires, fermetures, correspondances de Galois
• Symmetric quotients and domain constructions
• The weakest prespecification
• Varieties of relation algebras

Cited in

(4)

• Parallel composition and decomposition of specifications
• Nondeterministic semantics of compound diagrams
• Invariant relations for affine loops
• Embedding a demonic semilattice in a relation algebra

This page was built for publication: A relational division operator: The conjugate kernel

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