Инварианты и замеры
Вы узнаете
Как пишутся блоки invariant и bench и кто их вычисляет.
invariant с именем и следующим assert задаёт правило спеки, которое верно для любого значения, а не для одного примера. bench с именем отмечает блок для замера времени. Оба компилируются. Тестовый прогон этого сайта вычисляет только блоки test: инварианты и замеры он пропускает, так что ложный инвариант здесь проходит молча. Поэтому спека урока повторяет свой инвариант тестом.
Попробуйте
Сделайте инвариант ложным в плеере и убедитесь, что этот сайт молчит, затем сделайте ложным тест.
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;
}
Все уроки
Модуль 1 · Файл спеки
Что лежит в файле .t27: строка module, строки прозы и комментарии.
Модуль 2 · Значения и типы
Константы, ширина целого числа, а также true, false и текст.
Модуль 3 · Массивы, триты и выражения
Списки значений, три значения трита и что вычисляют операторы.
Модуль 4 · Тесты и функции
Блок test, несколько маленьких тестов в одной спеке и функция с типизированными входами.
Модуль 5 · Внутри функции
Имена через let и var, выбор через if и switch и циклы.
Модуль 6 · Видимость и свои типы
Что pub открывает другим модулям, и структуры и перечисления, которые вы объявляете.
Модуль 7 · Модули, правила и gen-ts
Чтение другого модуля, правило, которое выполняется всегда, и спека, превращённая в TypeScript.
Модуль 8 · Компилятор и tri
Бэкенды, которые пишет t27c, стадии, в которых он читает спеку, и команда tri.
Модуль 9 · Ошибки, программа и что дальше
Как читать ошибку компилятора, одна маленькая законченная программа и какой курс пройти дальше.