Invariants and benches
You will learn
How invariant and bench blocks are written and who evaluates them.
invariant name followed by an assert states a rule of the spec that must hold for every value, not one example. bench name marks a block to time. Both compile. The test runner on this site evaluates test blocks only: it skips invariants and benches, so a false invariant passes here silently. The lesson spec repeats its invariant as a test for that reason.
Try it
Make the invariant false in the player and check that nothing on this site complains, then make the test false.
The three kinds of checking block in t27 and which ones the site test runner evaluates. Lesson 20 of the t27 basics course.
specs/basics/20_invariants.t27
// SPDX-License-Identifier: Apache-2.0
; t27 basics, lesson 20: Invariants and benches.
; An invariant states a rule that must always hold; a bench names a measurement.
module basics_20_invariants;
pub const SIDES : u8 = 3;
invariant a_triangle_has_three_sides
assert SIDES == 3
test the_invariant_as_a_test {
assert SIDES == 3;
}
All lessons
Module 1 · A spec file
What a .t27 file holds: a module line, prose lines and comments.
Module 2 · Values and types
Constants, the width of a whole number, and true, false and text.
Module 3 · Arrays, trits and expressions
Lists of values, the three values of a trit, and what operators compute.
Module 4 · Tests and functions
A test block, several small tests in one spec, and a function with typed inputs.
Module 5 · Inside a function
Names with let and var, choices with if and switch, and loops.
Module 6 · Visibility and your own types
What pub shares with other modules, and the structs and enums you declare.
Module 7 · Modules, rules and gen-ts
Reading another module, stating a rule that always holds, and a spec turned into TypeScript.
Module 8 · The compiler and tri
The backends t27c writes, the stages it reads a spec in, and the tri command.
Module 9 · Errors, a program, what next
Reading a compiler error, one small complete program, and the course to take next.