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