NL → Constraints

A requirement describes a property. A constraint is that property, stated formally enough to evaluate. The translation is lossless when done right — the constraint says exactly what the English said, no more, no less.

Target formalisms

Pick based on what you're constraining:

English → logic — the mapping table

Worked example — data constraint

Requirement: "A valid user record has a username (3–32 alphanumeric characters, starting with a letter), an email containing exactly one @, an age of at least 13, and an optional bio of at most 500 characters."

Decompose:

As JSON Schema:

{
  "type": "object",
  "required": ["username", "email", "age"],
  "properties": {
    "username": { "type": "string", "pattern": "^[A-Za-z][A-Za-z0-9]{2,31}$" },
    "email":    { "type": "string", "pattern": "^[^@]*@[^@]*$" },
    "age":      { "type": "integer", "minimum": 13 },
    "bio":      { "type": ["string", "null"], "maxLength": 500 }
  },
  "additionalProperties": false
}

As a property-based test generator (Hypothesis):

from hypothesis import strategies as st

valid_user = st.fixed_dictionaries({
    "username": st.from_regex(r"^[A-Za-z][A-Za-z0-9]{2,31}$", fullmatch=True),
    "email":    st.from_regex(r"^[^@]+@[^@]+$", fullmatch=True),
    "age":      st.integers(min_value=13),
    "bio":      st.one_of(st.none(), st.text(max_size=500)),
})

Same constraint, three formalisms. Pick the one your tooling consumes.

Worked example — behavioral constraint

Requirement: "The sort function returns a permutation of its input in non-decreasing order."

Two constraints:

1. Permutation: Counter(output) == Counter(input) — same elements, same multiplicities.
2. Ordered: all(output[i] <= output[i+1] for i in range(len(output)-1)).

As a property test:

from collections import Counter
from hypothesis import given, strategies as st

@given(st.lists(st.integers()))
def test_sort_is_ordered_permutation(xs):
    result = sort(xs)
    assert Counter(result) == Counter(xs)                            # permutation
    assert all(result[i] <= result[i+1] for i in range(len(result)-1))  # ordered

This is the requirement, executable. Any sort that passes this test satisfies the requirement. Any sort that fails violates it.

The "only if" trap

English conditionals don't map to logic the way they sound:

"Access granted only if authenticated" = access → authenticated. It does NOT say authenticated users get access — that would be "access granted if authenticated."

Do not

• Do not translate ambiguous English. If → ambiguity-detector would flag it, resolve the ambiguity before formalizing. A precise formalization of an ambiguous requirement is precisely wrong.
• Do not over-constrain. "Email must contain @" → .*@.* is right. ^[a-z]+@[a-z]+\.[a-z]+$ is wrong — the requirement didn't say any of that.
• Do not under-constrain. "Exactly one @" needs both "at least one" and "at most one." .*@.* gives you only the first.
• Do not mix "only if" with "if." They're converses. Wrong direction = the constraint says the opposite of the requirement.

Output format

## Requirement (verbatim)
<text>

## Decomposition
| Clause | Constraint (logic) |
| ------ | ------------------ |

## Formalization
Target: <JSON Schema | predicate | property test | temporal logic>
<code>

## Faithfulness check
- Over-constrains? <anything the formalization forbids that the English allows>
- Under-constrains? <anything the English forbids that the formalization allows>
- Direction check: <for each conditional — if/only-if/unless resolved correctly>