DigitableCourses
Локально и без аккаунта. Аккаунта нет, регистрация не нужна: введённое в инструменты остаётся в localStorage браузера и на сервер не уходит.
Свой счётчик считает открытия страниц и дочитывания: уезжает адрес и десятая доля текста. Без cookies и чужих счётчиков, IP не хранится, Do Not Track уважается. Как это проверить
Репозиторий портала не выложен, «открытым кодом» мы его не зовём. Открыто это:
Живёт портал на донатах, платных консультациях и разборах по запросу и покупке Workbench.
Планов делать курсы платными нет.
Выкладка от 8 ноября 2026, срез 8f78b0c
Что изменилось на портале с вашего прошлого захода.
Заданий: 8
Напишите функцию. Запустите примеры и проверку доказательств.
К вашему коду проверка дописывает утверждения задания (их видно под полем) и запускает flang check --proof. Задание засчитано, когда компилятор ответил кодом 0: всё разобрано, примеры сошлись, всё доказано. Компилятор скачивается со страниц языка при первой проверке — около 10 МБ, дальше он берётся из кеша браузера; текст вашего решения никуда не уходит. Те же задания с пояснениями — на странице практикума.
buildРегистрации на портале нет и не будет. Состояние живёт в вашем браузере (localStorage, ключи digitable:learn:*) и никуда не отправляется: ни один ответ не уходит на сервер, проверка целиком идёт здесь.
Функция «Квадрат» сейчас всегда отвечает 0. Напишите тело так, чтобы она возвращала н, умноженное на само себя.
утверждение «квадрат трёх — девять»
утверждаем («Квадрат» от 3) равно 9
утверждение «квадрат минус четырёх — шестнадцать»
утверждаем («Квадрат» от -4) равно 16Умножение пишется словами: н умножить на н.
«Модуль» обещает результат не меньше нуля, но сейчас просто возвращает х. Добавьте ветвление, чтобы ответ был верным и обещание доказывалось.
утверждение «модуль минус пяти — пять»
утверждаем («Модуль» от -5) равно 5
утверждение «модуль семи — семь»
утверждаем («Модуль» от 7) равно 7если х меньше 0, то 0 минус х, иначе х. Компилятор знает условие ветки внутри каждой ветки.
Светофор переключается так: красный → зелёный → жёлтый → красный. Напишите «Следующий» через разбор по вариантам.
утверждение «после красного — зелёный»
утверждаем («Следующий» от вариант Красный) равно вариант Зелёный
утверждение «после зелёного — жёлтый»
утверждаем («Следующий» от вариант Зелёный) равно вариант Жёлтый
утверждение «после жёлтого — красный»
утверждаем («Следующий» от вариант Жёлтый) равно вариант Красныйразбор сигнал, затем «случай Красный» и «то вариант Зелёный» для каждого варианта.
Посчитайте сумму элементов списка. Циклов в языке нет — нужна свёртка.
утверждение «сумма пустого списка — ноль»
утверждаем («Сумма» от пустой список) равно 0
утверждение «один, два, три — шесть»
утверждаем («Сумма» от [1, 2, 3]) равно 6свёртка элементы начиная с 0 как акк и эл → акк плюс эл
Скидка 500 положена заказу от 10 000, меньшим заказам скидки нет. Скидка не может быть больше суммы — это обещание должно доказываться.
утверждение «с 12 000 скидка 500»
утверждаем («Скидка» от 12000) равно 500
утверждение «с 2 000 скидки нет»
утверждаем («Скидка» от 2000) равно 0Ветка по условию «сумма не меньше 10000»; в ветке «то» компилятор знает, что 500 не больше суммы.
Компилятор отказывается принять «Сумма до»: рекурсия не уменьшает аргумент, и функция зациклится. Исправьте вызов.
Рекурсивно звать нужно с меньшим числом: («Сумма до» от (н минус 1)).
Проверка добавит функцию «Через удвоение» и теорему, которая ссылается на свойство «удвоение длины не меняет» функции «Удвоить все». Объявите это свойство.
тотальная функция «Через удвоение»
принимает элементы: список числа
возвращает список числа
для всех элементы обеспечивает «через удвоение длина та же» (длина результат) равен (длина элементы)
«Удвоить все» от элементы
теорема «через удвоение длина та же»
дано элементы: список числа
утверждаем (длина результат) равен (длина элементы)
по свойству «удвоение длины не меняет»
следовательно доказанодля всех элементы обеспечивает «удвоение длины не меняет» (длина результат) равен (длина элементы)
Допишите тело индукционного шага в теореме «шаг растит счёт на один».
В случае «Следующий» запишите «то по предположению».