Cink-maude

Various formal specifications of a very simple programming language (Cink) in Maude, including big-step semantics, smal--step semantics, symbolic execution, and Floyd-Hoare logic.

High-level documentation for the Maude repository and the contained modules.

🚀 Purpose

This repository provides a small imperative language core (Cink) with:

• syntax, expressions, statements, functions
• concrete operational semantics (small-step + big-step)
• symbolic execution plus SMT support
• state, arrays, and Hoare/floyd reasoning testbed modules

📁 Structure

• cink-syntax.maude: CinK grammar and AST (expressions, statements, programs)
• cink-programs.maude: top-level CINK-PROGRAMS includes syntax and lets tests invoke programs
• pl-builtins.maude: core value types
  • PL-BOOL: boolean algebra with true, false, andBool, orBool, notBool
  • PL-INT: integer operations +Int, *Int, -Int, /Int, comparisons
  • PL-ID: identifier names and lists extracted from BOTTOM, UNDEFINED
• array.maude: integer-array operations and selectors/update
• state.maude, state-smt.maude: imperative state maps from Id → values; SMT-aware variant (uses numeric SMT types)
• pl-set.maude: generic set constructors for List/Set (used by variable lists and declarations)

Semantics modules

• cink-smallstep/cink-semantics-smallstep.maude: small-step operational semantics using o (single step), * (multi-step) over labelled configurations
• cink-bigstep/cink-semantics-bigstep.maude: big-step (natural semantics) evaluator with => relations
• cink-smallstep/cink-smallstep.maude: test harness includes CINK-SEMANTICS-SMALLSTEP + CINK-PROGRAMS
• cink-bigstep/cink-bigstep.maude: test harness includes CINK-SEMANTICS-BIGSTEP + CINK-PROGRAMS

Symbolic execution

• symbolic/cink-smallstep/cink-semantics-smallstep-symbolic.maude: symbolic small-step semantics with path condition (Assert) and SMT interaction
• symbolic/cink-smallstep/cink-smallstep-symbolic.maude: entrypoint module for proof/test harness with symbolic semantics

SMT and theorem-engine plumbing

• smt-pl.maude: SMT integration definitions
  • SMT-CONV: conversion between PL terms and SMT terms
  • BOOLEAN, INTEGER, REAL, REAL-INTEGER mapping
  • SUBST: substitution operations

Floyd-Hoare logic / verification utilities

• floyd-hoare-logic/veco.maude: vector calculus helpers (likely used by proof obligations)
• floyd-hoare-logic/tableaux.maude: tableau-based reasoning infrastructure
• floyd-hoare-logic/smt-test.maude: sample verification tests using SMT + semantics