Верификатор

Cтраница 1

Верификаторы служат для проверки правильности пробивок на перфокартах. [1]

Если это заявление соответствует истине и если считать верификатор lint частью официального описания языка Си, то с языком Си дело обстоит не так плохо, как утверждал автор выше. К сожалению, детали проверок, выполняемых верификатором lint, нигде и никак не документированы. [2]

Проверка правильности нанесения на перфокарту сведений проводится на верификаторе ( контрольнике), операция проверки носит название верификации. [3]

Гчытк ш тол ен чя специальной машине, называемой верификатором, или же на машине, которую можно переключать из режима подготовки данных в режим верификации и обратно. При использовании таких носителей, как перфолента или перфокарты, на которых закодированные данные не могут быть изменены, обычно применяются отдельные машины-верификаторы. При записи данных на магнитных носителях для обоих процессов может быть использовано одно и то же устройство, которым могут быть клавиатура с дисплеем, соединенная с системой. [4]

Следующим шагом в сервисе обеспечения переносимости готовых программ является применение верификаторов, фильтров и конверторов. Фильтры и верификаторы - это программы, выполняющие проверку заданных наборов правил, соответствующих входному языку, на который осуществляется перенос программы. Назначение этих систем заключается в исследовании текстов программ, написанных для единого входного языка с точки зрения правильности, и синтаксиса при трансляции на другой входной язык. Ниже приводится описание системы Фильтр, разработанной в ЛИИАН в ОС ЕС для анализа текстов, написанных на языке Фортран. Побочным применением данной системы является обучение пользователя особенностям программирования на языке Фортран. Система обладает свойствами экспертности, поэтому в дальнейшем будем ее называть экспертной системой ( ЭС) Фильтр. ЭС Фильтр состоит из базы знаний, диалогового процессора во взаимодействии с пользователем, блока объяснения действий системы, блока извлечения знаний и блока взаимодействия с инженером-интерпретатором. [5]

Следует еще раз остановиться на вопросе о том, какую роль играет верификатор lint. [6]

В состав системы ДЕМОС входят: компилятор с языка СИ и отладчик; верификатор программ на языке СИ; языковые процессоры, в том числе БЕЙСИК и ФОРТРАН-77; редакторы текстов ( строковый, экранный, потоковый); средства построения компиляторов; средства связи между пользователями; средства обработки текстов и подготовки документации; средства ведения версификационной работы, обеспечивающие запись, поиск и хранение версий текстовых файлов, позволяющие вести учет изменений и контролировать доступ к файлам при одновременной работе нескольких пользователей. [7]

МЯ становится языком, в котором мы можем строить средства манипулирования программами, такие как интерпретаторы, верификаторы, редакторы или операционные системы. Метаязык, несомненно, может многое дать для формализации, и реализации таких задач, как построение программ, их анализ и исполнение, - короче говоря, для технологии программного обеспечения. Особенно интересным является тот факт, что метаязык может сам быть просто языком логики хорновских дизъюнктов, и, таким образом, его можно реализовать при помощи уже имеющихся логических реализаций. Эта мощная двойственная роль логики была обнаружена и использована уже на раннем этапе развития логического программирования: простые интерпретаторы, написанные на обычных языках программирования, применялись для того, чтобы посредством раскрутки получить более совершенные версии, которые сами были написаны ( что более удобно) на языке логики и которые содержали мета-уровневые описания того, как должны исполняться другие логические программы. [8]

Граф управляющей логики для функции / I a. [9]

В настоящее время доступно несколько программ для автоматического анализа исходного кода на языке C / C, которые могут оказать помощь разработчикам и верификаторам ПО. [10]

Хотя язык Си и нельзя считать языком программирования с сильной типизацией, тем не менее программа, написанная на языке Си, в которой не выявлено ошибок верификатором lint, по-видимому, может считаться написанной на языке программирования с сильной типизацией. [11]

Программисты быстро привыкают использовать скобки во всех сомнительных случаях. Кроме того, верификатор lint предупреждает обо всех сомнительных ( с его точки зрения) выражениях, каковыми, в частности, являются оба приведенных выше примера. [13]

Существует еще один компонент программного обеспечения, который имеет прямое отношение к языку Си и который по этой причине обязательно должен быть упомянут в настоящем обсуждении. Речь идет о верификаторе lint [93], который, как сказано в книге [101] ( с. Верификатор lint обеспечивает выявление и диагностику множества настоящих и предполагаемых ошибок, выявление и диагностику которых большая часть трансляторов с языка Си даже не пытается произвести. [14]

Хотя в языке Си имеются типы данных ( в отличие от его предшественника - языка BCPL) и большинство трансляторов с языка Си обеспечивает проведение в том или ином объеме контроля типов, тем не менее утверждать, что язык Си является языком программирования с сильной типизацией было бы неверно. На самом деле основной функцией верификатора lint является выявление нарушений контроля типов, не выявляемых трансляторами с языка Си. Язык Си предоставляет в распоряжение программиста множество возможностей для нарушения контроля типов. Некоторые из этих возможностей перечислены ниже. [15]

Страницы: 1 2