Axiom Logi c и формальные методы - PullRequest
0 голосов
/ 30 мая 2020

У меня острая проблема. Я новичок в дискретной математике, и я пытался исследовать приведенный ниже вопрос, но, похоже, я зашел в тупик. Я был бы признателен за любую подсказку о том, как ее решить. часть кодирования, которую я могу реализовать.

Учитывая определение аксиомы функции p, описанное ниже: для натурального числа n, p отображает n в простое число n. Рассмотрим упрощенный пример управления библиотекой: пусть [Book] будет типом, который содержит все книги , и пусть Library == Book +> N Используйте Lib: Library, чтобы указать состояние текущей библиотеки в библиотеке, т.е. для любой книги x, lib (x) представляет текущее количество x в библиотеке. Используйте определение аксиомы для описания следующих операций: 1. заимствовать (lib, x): заимствовать книгу x из библиотеки lib, значение новой библиотеки 2. return (lib, x): вернуть книгу x в библиотеку lib, значение новой библиотеки 3.Inlibrary (lib): запрос библиотеки, значение - это коллекция для всех книг в библиотеке, число которых больше 0

...