Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Operational semantics and program verification using many-sorted hybrid modal logic

Ioana Leustean, Natalia Moanga, Traian Florin Serbanuta

TL;DR

This work develops a general, sound, and complete many-sorted hybrid modal logic as a unified framework to specify operational semantics and perform program verification. By introducing constant nominals and state variables, it enables precise, cross-sort reasoning about program execution and verification within ${\mathcal{H}}_{\bf Σ}(@)$ and ${\mathcal{H}}_{\bf Σ}(@,\forall)$. A concrete SMC-like language is then encoded, and a Hoare-like calculus is derived, including rules for conditionals and loops, demonstrated via a detailed correctness proof of a simple summation program. The approach promises more natural semantic descriptions and tighter integration between language semantics and verification, with solid theoretical guarantees and avenues for future extensions and applications.

Abstract

We propose a general framework to allow: (a) specifying the operational semantics of a programming language; and (b) stating and proving properties about program correctness. Our framework is based on a many-sorted system of hybrid modal logic, for which we prove completeness results. We believe that our approach to program verification improves over the existing approaches within modal logic as (1) it is based on operational semantics which allows for a more natural description of the execution than Hoare's style weakest precondition used by dynamic logic; (2) being multi-sorted, it allows for a clearer encoding of semantics, with a smaller representational distance to its intended meaning.

Operational semantics and program verification using many-sorted hybrid modal logic

TL;DR

This work develops a general, sound, and complete many-sorted hybrid modal logic as a unified framework to specify operational semantics and perform program verification. By introducing constant nominals and state variables, it enables precise, cross-sort reasoning about program execution and verification within and . A concrete SMC-like language is then encoded, and a Hoare-like calculus is derived, including rules for conditionals and loops, demonstrated via a detailed correctness proof of a simple summation program. The approach promises more natural semantic descriptions and tighter integration between language semantics and verification, with solid theoretical guarantees and avenues for future extensions and applications.

Abstract

We propose a general framework to allow: (a) specifying the operational semantics of a programming language; and (b) stating and proving properties about program correctness. Our framework is based on a many-sorted system of hybrid modal logic, for which we prove completeness results. We believe that our approach to program verification improves over the existing approaches within modal logic as (1) it is based on operational semantics which allows for a more natural description of the execution than Hoare's style weakest precondition used by dynamic logic; (2) being multi-sorted, it allows for a clearer encoding of semantics, with a smaller representational distance to its intended meaning.

Paper Structure

This paper contains 6 sections, 16 theorems, 1 equation, 3 figures.

Table of Contents

  1. Introduction
  2. Preliminaries: a many-sorted modal logic
  3. Many-sorted hybrid modal logic
  4. A SMC-like language and a Hoare-like logic for it
  5. Proving a program correct.
  6. Conclusions and related work

Key Result

Theorem 2.3

noi Let $\Gamma_s$ be a set of formulas of set $s$. If $\Gamma_s$ is a consistent set in ${\mathbf K}_{\bf \Sigma}$ then $\Gamma_s$ has a model. Moreover, if $\phi$ is a formula of sort $s$, then $\Gamma_s\models_{{\mathbf K}_{\bf\Sigma}}\phi$ iff $\Gamma_s\vdash_{{\mathbf K}_{\bf\Sigma}}\phi$, wher

Figures (3)

  • Figure 1: $(S,\Sigma)$ modal logic
  • Figure 2: $(S,\Sigma)$ hybrid logic
  • Figure 3: Axioms defining an SMC-like programming language

Theorems & Definitions (45)

  • Definition 2.1: Validity and satisfiability
  • Definition 2.2: Local deduction
  • Theorem 2.3
  • Remark 2.4: Problems
  • Definition 3.1: Signature with constant nominals
  • Definition 3.2: Formulas
  • Remark 3.3: Expressivity
  • Definition 3.4
  • Definition 3.5: The satisfaction relation in ${\mathcal{H}}_{\bf \Sigma}(@)$
  • Definition 3.6: The satisfaction relation in ${\mathcal{H}}_{\bf \Sigma}(@,\forall)$
  • ...and 35 more