2016-04-07 5 views
7

В настоящее время я изучаю проверку модели (модальная логика, LTL, CTL, SAL model checker и т. Д.), И в свободное время я изучаю Idris, который является строго типизированным функциональным языком программирования, который поддерживает зависимые типы. Поскольку я рассматриваю как проверку модели, так и Идрис, я начинаю любопытно, как Идрис относится к формальным методам и проверке модели.Релевантность проверки модели в строго типизированных функциональных языках программирования?

Когда вы узнаете о проверке модели, кажется, что большинство примеров, поднятых, - это либо проверка систем, написанных императивным образом, либо аппаратных компонентов. Поэтому я озадачен релевантностью проверки модели на строго типизированных языках функционального программирования и, особенно, на зависимом типизированном языке, таком как Идрис, где мне кажется, что проверяющий тип уже делает фантастическую работу по проверке правильности. Моя интуиция, однако, говорит мне, что проверка модели может быть связана с частичными функциями, которые не дают никаких обещаний о прекращении.

Является ли проверка модели актуальной при использовании строгого и зависимого типизированного языка программирования, такого как Идрис?

ответ

2

Вы правы, что проверка модели чаще всего используется для проверки аппаратных средств и императивных (часто параллельных) программ, поскольку ее происхождение также находится в этой области. Для функциональных программ широко используются методы проверки типов. Тем не менее, они часто требуют много аннотаций или могут создавать «ложные срабатывания», что приводит к опровержению «правильной» программы. Проверка модели не требует этих аннотаций, а также позволяет отвечать на более конкретные вопросы. Я не эксперт в этой области, но кажется, что методы из систем типов и проверки модели часто объединяются для функциональных программ. Если вы заинтересованы в текущих исследованиях и подходы к модели Проверки функциональных программ, есть отличный курс с большим количеством материала в Интернет:

http://www.cs.ox.ac.uk/people/luke.ong/personal/EWSCS13

Курс был подготовлен Люк Ong, один из ведущих исследователей в этой области.