Мне нравится все, что происходит во время компиляции, и мне нравится идея, что, как только вы скомпилируете программу, вы получите много гарантий относительно ее выполнения. Вообще говоря, статическая система типов (Haskell, C ++, ...), похоже, дает более сильные гарантии во время компиляции, чем любая система динамических типов.
Из того, что я понимаю, Ada идет еще дальше в отношении проверки времени компиляции и может обнаружить больший диапазон ошибок до выполнения. Это также считается довольно безопасным, учитывая, что в какой-то момент он был выбран для деликатных полей (когда ошибки программирования могут стоить человеческих жизней).
Теперь я задаюсь вопросом: если более сильные статические гарантии приводят к более документированному и безопасному коду, то почему мы не исследуем больше в этом направлении?
Примером чего-то, что, по-видимому, отсутствует, может быть язык, в котором вместо определения универсального int
типа с диапазоном, определяемым числом битов базовой архитектуры, можно использовать диапазоны (в следующем примере Int [a..b]
описывается целочисленный тип между А и В включены):
a : Int [1..24]
b : Int [1..12]
a + b : Int [2..36]
a - b : Int [-11..23]
b - a : Int [-23..11]
или (принимая это от Ады):
a : Int [mod 24]
b : Int [mod 24]
a + b : Int [mod 24]
Этот язык выберет лучший базовый тип для диапазона и выполнит проверку времени компиляции для выражений. Так что, например, дано:
a : Int [-3..24]
b : Int [3..10]
тогда:
a / b
никогда не будет не определено.
Это всего лишь пример, но я чувствую, что во время компиляции мы можем применить намного больше. Так почему же здесь так мало исследований? Каковы технические термины, которые описывают эту идею (чтобы я мог найти больше информации по этой теме)? Каковы пределы?
dependent type
илиrefinement type
.Ответы:
Я не в состоянии сказать , сколько еще исследование должно быть сделано по этой теме, но я могу сказать вам , что это исследование делается, например, Verisoft XT программа финансируется правительством Германии.
Концепции, которые, я думаю, вы ищете, называются формальной верификацией и программированием на основе контрактов , где последний является удобным для программиста способом сделать первый. В программировании на основе контрактов вы сначала пишете свой код как обычно, а затем вставляете в код так называемые контракты . Легко используемым языком, основанным на этой парадигме, является Spec # от Microsoft Research и функционально похожее, но немного менее симпатичное расширение Code Contracts для C #, которое вы оба можете попробовать онлайн (у них также есть аналогичные инструменты для других языков, см. Rise4fun) ). Упомянутый вами тип int с типом диапазона будет отражен двумя контрактами в функции:
Если вы хотите вызвать эту функцию, вам нужно будет использовать параметры, которые соответствуют этим критериям, или вы получите ошибку времени компиляции. Выше очень простые контракты, вы можете вставить практически любое предположение или требование о переменных или исключениях и их отношениях, о которых вы можете подумать, и компилятор проверит, покрывается ли каждое требование предположением или чем-то, что может быть обеспечено, т.е. из предположений. Вот почему, откуда исходит название: вызывающий абонент предъявляет требования , вызывающий обеспечивает их выполнение - как в деловом контракте.
Под капотом контракты кода обычно объединяются со знанием внутренней работы (операционной семантики) языка программирования в список условий проверки . Этот список представляет собой одно большое логическое предложение с свободными переменными - входами вашей программы. Если предложение верно для всех возможных назначений переменных, то программа считается правильной. Чтобы проверить, так ли это, SMT Proverп РP(x1,x2,...,xn) n P используется. Со стороны CS, эти два являются критическими частями процесса - генерация условий проверки является сложной, а SMT является либо NP-полной, либо неразрешимой проблемой, в зависимости от рассматриваемых теорий. Существует даже соревнование для специалистов по SMT, так что, безусловно, есть некоторые исследования в этом направлении. Кроме того, существуют альтернативные подходы к использованию SMT для формальной проверки, такие как перечисление пространства состояний, проверка символьной модели, проверка ограниченной модели и многие другие, которые также исследуются, хотя SMT, на самом деле, в настоящее время является наиболее «современным» подходом.
Относительно границ общей идеи:
Последнее, что стоит упомянуть и которое не совсем соответствует приведенному выше объяснению, - это поле, называемое «Теория неявной сложности», например, эта статья . Он нацелен на характеристику языков программирования, в которых каждая программа, которую вы можете написать, попадает в определенный класс сложности, например P. В таком языке каждая написанная вами программа автоматически «гарантированно» имеет полиномиальное время выполнения, которое можно «проверить» во время компиляции, просто компилируя программу. Однако я не знаю каких-либо практически применимых результатов этого исследования, но я также далек от того, чтобы быть экспертом.
источник