Бібліотека Київського столичного університету імені Бориса Грінченка

Головна

Спрощенний режим

Посібник користувача

Бази даних

Електронний каталог бібліотеки- результати пошуку

Вид пошуку

Електронний каталог бібліотеки

Каталог авторефератів та дисертацій

Грінченкознавство

Рідкісні та цінні видання

Українська Аудіокнига

Мережеві ресурси

Наукові періодичні видання Університету

Зона пошуку

Формат представлення знайдених документів:
повний	інформаційний	короткий

Пошуковий запит: (<.>K=практика програмування<.>)

Загальна кількість знайдених документів : 1

004.43(07)Agda
S90

Stump, Aaron David.
Verified Functional Programming in Agda / A. D. Stump ; Association for Computing Machinery. - New York : ACM Books, 2016. - 258 p. - (ACM Books series ; #9). - ISBN 978-1-970001-27-3 : Б. ц.
Переклад назви: Перевірено функціональне програмування в Agda

ДРНТІ	20
УДК	004.43(07)Agda

Рубрики: Мови програмування--Agda--Навчальні видання

Кл.слова (ненормовані):
зовнішня перевірка -- внутрішня перевірка -- практика програмування -- якість програмного забезпечення
Анотація: Agda - це передова мова програмування, заснована на типу теорії. Система типу Agda є достатньо виразною, щоб підтримувати повну функціональну перевірку програм у двох стилях. Під час зовнішньої перевірки ми пишемо чисті функціональні програми, а потім пишемо докази властивостей про них. Докази - це окремі зовнішні артефакти, як правило, з використанням структурної індукції. Під час внутрішньої перевірки ми визначаємо властивості програм через розширені типи для самих програм. Це часто вимагає включення доказів всередині коду, щоб показати перевірку типу, що вказані властивості містять. Можливість доказувати властивості програм у цих двох стилях - це глибоке доповнення до практики програмування, що дає програмістам можливість гарантувати відсутність помилок і тим самим покращувати якість програмного забезпечення більш ніж раніше можливо. Перевірене функціональне програмування в Агді - це перша книга, в якій подано систематичну експозицію зовнішньої та внутрішньої перевірки в Агді, що підходить для студентів магістратури з інформатики. Не передбачається ознайомлення з функціональним програмуванням або перевіреними комп'ютером доказами. Книга починається з ознайомлення з функціональним програмуванням через звичні приклади, такі як булеві, натуральні числа, списки та методи зовнішньої перевірки. Внутрішня перевірка розглядається на прикладах векторів, дерев бінарного пошуку та дерев Браун. Також входить більш досконалий матеріал щодо обчислення на рівні типу, чітких міркувань щодо припинення та нормалізації шляхом оцінки. Книга також включає середній розмірний випадок кодування та декодування Хаффмана.

Дод.точки доступу:
Association for Computing Machinery

Примірників всього: 1
Сервер (1)
Вільні:
Сервер (1)

Знайти схожі

© Міжнародна Асоціація користувачів і розробників електронних бібліотек і нових інформаційних технологій
(Асоціація ЕБНІТ)