Laws (Bend 2)

Question: Does the comment above a law promise more than, or something other than, what the law states, so a definition could break the promise while every proof passes?

• Runs: by default · Fails the check by default: no
• Right on projects JevGate was never tuned on: not measured (how it is measured)
• Right on the projects it was tuned on: not measured
• Looks at: Bend 2 laws that state a claim (an equality, a witness or a proposition) under a comment, outside tests
• Evidence unit: one law with its comment and the signatures, documentation and short bodies of the definitions it names
• Acceptable: A comment that puts its law in words; laws that declare a signature or a primitive
• Names: tests/laws, laws, laws · Version: 1

When a finding is right

A law is the part of a Bend 2 specification the compiler checks, and its comment the part a person reads. A finding says the comment above a law promises more than, or something other than, what the law states, so a definition could break the promise while every proof passes. It is right when the comment names a property, a case or a condition the law leaves out: bend-json’s remove_sound checks a one-entry object under “remove deletes key from object”. It is wrong when the law states the comment in other words, or when a sibling law states the rest. More than half of the findings labeled wrong or debatable were laws stating their comment in other words.

The accuracy table leaves Bend 2 projects out, so the rule shows as not measured there. When it shipped in 0.22.0, law findings were right 15 times in 23 on Bend 2 projects never used for tuning.

Findings it got wrong

Labeled wrong by reading the code, on open-source Bend 2 projects the rules were tuned on.

Bend: press_reads

• Where: demos/app_ray_tracer_3d/LAWS.bend:14 in bendlang/bend at 574b6d3.
• Finding (consider): The comment above law press_reads promises more than the law states. A definition could break that promise while every proof passes.
• Why it was wrong: The law states Ray.Fly.get(Ray.Fly.set(held, k, v), k) == v for every list of held keys, slot and value: the comment’s “that key reads pressed (or released), for any slot and any held keys” in other words.
• Since: not addressed; reported the same way from 0.22.0 through 0.24.1, the latest release run on the Bend 2 projects.

bolt: trace_pending_judged

• Where: src/rules/LAWS.bend:228 in Emerging-Patterns/bolt at 85f175d.
• Finding (review): The comment above law trace_pending_judged promises more than the law states. A definition could break that promise while every proof passes.
• Why it was wrong: The law states the comment’s main clause exactly: a pending row naming laws is judged as a proved row naming the same laws. The comment’s other clauses are stated by sibling laws: trace_pending_shape and trace_proved_shape right after it, and trace_counts further down.
• Since: not addressed; reported the same way from 0.22.0 through 0.24.1, the latest release run on the Bend 2 projects.

bolt: walk_bfs

• Where: src/LAWS.bend:749 in Emerging-Patterns/bolt at 85f175d.
• Finding (review): The comment above law walk_bfs promises more than the law states. A definition could break that promise while every proof passes.
• Why it was wrong: The law equates the walk’s result with found_in(bfs(…)), a model written just above it in LAWS.bend. Every clause of the comment, the bound on directories read, hidden and node_modules directories skipped, nothing past the bound, is a clause of that model, so no walk could break it while the law holds.
• Since: not addressed; reported the same way from 0.22.0 through 0.24.1, the latest release run on the Bend 2 projects.