Natural Hoare Logic: Towards formal verification of programs from logical forms of natural language specifications

TL;DR

This paper introduces Natural Hoare Logic, a framework that uses semantic parsing of natural language specifications to enable formal verification of software, bridging natural language requirements and program correctness.

Contribution

It presents a novel formal verification framework that integrates semantic parsing of natural language assertions with Hoare logic for software correctness verification.

Findings

Framework enables verification against natural language specifications

Addresses semantic parser errors with practical guarding methods

Extends Hoare logic to natural language-based assertions

Abstract

Formal verification provides strong guarantees of correctness of software, which are especially important in safety or security critical systems. Hoare logic is a widely used formalism for rigorous verification of software against specifications in the form of pre-condition/post-condition assertions. The advancement of semantic parsing techniques and higher computational capabilities enable us to extract semantic content from natural language text as formal logical forms, with increasing accuracy and coverage. This paper proposes a formal framework for Hoare logic-based formal verification of imperative programs using logical forms generated from compositional semantic parsing of natural language assertions. We call our reasoning approach Natural Hoare Logic. This enables formal verification of software directly against safety requirements specified by a domain expert in natural language. We consider both declarative assertions of program invariants and state change as well as imperative assertions that specify commands which alter the program state. We discuss how the reasoning approach can be extended using domain knowledge and a practical approach for guarding against semantic parser errors.