Table of Contents
Fetching ...

A Specification's Realm: Characterizing the Knowledge Required for Executing a Given Algorithm Specification

Assaf Marron, David Harel

TL;DR

This paper introduces the concept of the algorithm-specification realm, a finite repository of prerequisite knowledge needed to execute a given NL or pseudocode specification. It argues that the realm enables mechanical execution independent of a specific implementation and can be partly automated via large language models and existing documents. The authors outline the realm contents—language syntax/semantics, foundational model entities, relationships, domain causality rules, and instruction tools—and provide a constructive process for building the realm, with discussion on faithfulness, verification, and cross-system applicability. The work highlights the realm's potential to enhance formal verification, interpretability, and reusable execution across diverse systems, while distinguishing it from related modeling approaches like Problem Frames and signaling directions for future research.

Abstract

An algorithm specification in natural language or pseudocode is expected to be clear and explicit enough to enable mechanical execution. In this position paper we contribute an initial characterization of the knowledge that an executing agent, human or machine, should possess in order to be able to carry out the instructions of a given algorithm specification as a stand-alone entity, independent of any system implementation. We argue that, for that algorithm specification, such prerequisite knowledge, whether unique or shared with other specifications, can be summarized in a document of practical size. We term this document the realm of the algorithm specification. The generation of such a realm is itself a systematic analytical process, significant parts of which can be automated with the help of large language models and the reuse of existing documents. The algorithm-specification's realm would consist of specification language syntax and semantics, domain knowledge restricted to the referenced entities, inter-entity relationships, relevant underlying cause-and-effect rules, and detailed instructions and means for carrying out certain operations. Such characterization of the realm can contribute to methodological implementation of the algorithm specification in diverse systems and to its formalization for mechanical verification. The paper also touches upon the question of assessing execution faithfulness, which is distinct from correctness: in the absence of a reference interpretation of natural language or pseudocode specification with a given vocabulary, how can we determine if an observed agent's execution indeed complies with the input specification.

A Specification's Realm: Characterizing the Knowledge Required for Executing a Given Algorithm Specification

TL;DR

This paper introduces the concept of the algorithm-specification realm, a finite repository of prerequisite knowledge needed to execute a given NL or pseudocode specification. It argues that the realm enables mechanical execution independent of a specific implementation and can be partly automated via large language models and existing documents. The authors outline the realm contents—language syntax/semantics, foundational model entities, relationships, domain causality rules, and instruction tools—and provide a constructive process for building the realm, with discussion on faithfulness, verification, and cross-system applicability. The work highlights the realm's potential to enhance formal verification, interpretability, and reusable execution across diverse systems, while distinguishing it from related modeling approaches like Problem Frames and signaling directions for future research.

Abstract

An algorithm specification in natural language or pseudocode is expected to be clear and explicit enough to enable mechanical execution. In this position paper we contribute an initial characterization of the knowledge that an executing agent, human or machine, should possess in order to be able to carry out the instructions of a given algorithm specification as a stand-alone entity, independent of any system implementation. We argue that, for that algorithm specification, such prerequisite knowledge, whether unique or shared with other specifications, can be summarized in a document of practical size. We term this document the realm of the algorithm specification. The generation of such a realm is itself a systematic analytical process, significant parts of which can be automated with the help of large language models and the reuse of existing documents. The algorithm-specification's realm would consist of specification language syntax and semantics, domain knowledge restricted to the referenced entities, inter-entity relationships, relevant underlying cause-and-effect rules, and detailed instructions and means for carrying out certain operations. Such characterization of the realm can contribute to methodological implementation of the algorithm specification in diverse systems and to its formalization for mechanical verification. The paper also touches upon the question of assessing execution faithfulness, which is distinct from correctness: in the absence of a reference interpretation of natural language or pseudocode specification with a given vocabulary, how can we determine if an observed agent's execution indeed complies with the input specification.
Paper Structure (13 sections, 2 figures)

This paper contains 13 sections, 2 figures.

Figures (2)

  • Figure 1: The concept of an algorithm specification's realm. A mental conception of an algorithm (top left) is concretized in a specification document. The specification's realm, constructed specially for that specification as described in Sec. \ref{['sec:process']}, contains the knowledge required for executing that specification. The realm is only a finite subset of the unbounded information available for the various related disciplines. The executing agent --- human or machine --- receives both the algorithm specification and the realm constructed for it, and can then execute the specification repeatedly on diverse inputs.
  • Figure 2: Examples of algorithm specifications and their realms. For each algorithm specification, identified with its source in the first column, the second column describes the style and format of the specification. The third column contains informal statements of a few examples of additional facts and skills that are not part of the algorithm specification, and must be established in the specification's realm in order to enable an agent to execute it.