provable_contracts/schema/
clause.rs

1//! ONT-001 §5 ONT-4e — preconditions and postconditions as first-class clauses.
2//!
3//! `requires[]` and `ensures[]` sit beside `invariants[]` with one shape, `{id, statement, formal, formal_status}`
4//! (§3.5, the schema row: "`requires[]`/`ensures[]` beside `invariants[]` (ONT-4e), `*[].formal_status`"). The
5//! shape is closed: an unknown key is a parse error, so a misspelt `formal_satus` is refused, not silently read as a
6//! clause with no status.
7//!
8//! `formal_status` says whether `formal` is checkable: `parsed` clauses take part in the Liskov check on `refines`
9//! (R-20), `prose` clauses make it `Unknown{Prose}`. A `parsed` clause without a `formal` is a contradiction in
10//! terms and is refused by [`Clause::defect`].
11
12use serde::{Deserialize, Serialize};
13
14/// Whether a clause's `formal` is in the checkable subset.
15#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Serialize, Deserialize)]
16#[serde(rename_all = "lowercase")]
17pub enum FormalStatus {
18    /// `formal` is a proposition the Liskov check can compare.
19    Parsed,
20    /// `formal` is absent or not checkable; any check that meets it answers `Unknown{Prose}`.
21    Prose,
22}
23
24/// One `requires[]` / `ensures[]` entry (and an `invariants[]` entry that carries `formal_status`).
25#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
26#[serde(deny_unknown_fields)]
27pub struct Clause {
28    pub id: String,
29    pub statement: String,
30    #[serde(default, skip_serializing_if = "Option::is_none")]
31    pub formal: Option<String>,
32    pub formal_status: FormalStatus,
33}
34
35impl Clause {
36    /// Why this clause is not well formed, or `None`.
37    #[must_use]
38    pub fn defect(&self) -> Option<String> {
39        if self.id.trim().is_empty() {
40            return Some("empty id".into());
41        }
42        let formal_empty = self.formal.as_deref().is_none_or(|f| f.trim().is_empty());
43        (self.formal_status == FormalStatus::Parsed && formal_empty)
44            .then(|| format!("{}: formal_status parsed with no formal", self.id))
45    }
46
47    /// The proposition the Liskov check compares: `formal` with whitespace runs collapsed. `None` for prose.
48    #[must_use]
49    pub fn atom(&self) -> Option<String> {
50        match self.formal_status {
51            FormalStatus::Parsed => self
52                .formal
53                .as_deref()
54                .map(|f| f.split_whitespace().collect::<Vec<_>>().join(" ")),
55            FormalStatus::Prose => None,
56        }
57    }
58}
provable_contracts/schema/clause.rs

provable_contracts/schema/
clause.rs
