Первый этап - введение системы ненавязчивой статической типизации. А дальше — решаем проблемы по мере их поступления. Возможно пригодятся вариации на тему static assertion, алгебраические типы данных...

Отчего же большинство промышленных систем разработки используют верификаторы?


НУ, нужно спросить - каково происхождение этих проблем. Кто источник проблем а существование файла верифицировать можно.

да, действительно, речь идет о ловле зевков. Логика работы кода остается на совести программиста.

Потому что с этими системами работают много программистов (т.е. тех, кто использует инструменты, а не разрабатывает их), поэтому общий выигрыш в человеко-часах оказывается существенным.

Нет, это немного не то. Под верификацией понимается некий процесс, который, анализируя код, пытается понять, корректен ли он. Причем заранее понять, а не выполняя и наталкиваясь на проблемы.

Именно, и корректен ли файл (содержимое) или корректно ли указание на его наличие - тоже. Скажем, если я под GCC попытаюсь написать
#include no_present_file.my_fantasy
и компилятор выдаст мне error, то будет ли это верификацией кода?
в узком смысле -нет, т.к. верификация касается в основ. алгоритма и синтаксических момент ов
но если я использую несуществующее имя переменной чем это по сути отличалось бы от несуществующего имени файла?

поэтому и программисты одиночки тозже пользуются теми же ?

Нет, верификация касается других аспектов. Например, если я выделю память под переменную с плавающей точкой, а потом прочитаю содержимое через @, то программа будет синтаксически корректна, но вернет мне не округленное число, а двоичное представление числа с плавающей точкой. Или, объявив VARIABLE A VARIABLE B, я могу забыть, что это адреса, и вместо A @ B @ + написать A B +. Это тоже корректно с точки зрения языка, но не то, что я ожидал.

А их как бы никто и не спрашивает Системы верификации разрабатывают потому, что есть достаточное количество потребителей, а не потому что много одиночек были бы не против с таким поработать.

Я полагаю, и то и другое верификация, но понятно, что второе - более точно.

по всей видимости, верификацией хочется называть проверку правильности кода помимо синтаксиса ("более чем проверка синтаксиса")

времени не будет убито нисколько, ибо уже известны dup и *, а на их основе система сама сможет вывести тип, что-нибудь вроде ( n -- n' ) или даже ( n -- n*n ) или даже ( n -- n^2 ). гораздо более неприятны фрагменты вроде:



вот в таких местах и понадобятся аннотации от человека. кроме того, кто сказал, что надо обходиться только стековым комментарием? на самом деле в пакет для проверки следует включать стек возврата, переменную STATE (если более точно, то режимы исполнения/компиляции/отложенной_компиляции и т.п.)

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

Читал, читал... и ничего не понял (
Если речь идет о проверке уже готового ExE-файла, то тут все слова, что написаны в программе должны быть точками входа из вне.
Если же речь идет о верификации стековых диаграмм и написанного кода, то тут могу только посочувствовать идее в целом.
Вообще верификации ФОРТ-программ идет поэтапно на стадии разработки каждого нового слова вносимого в словарь, который может быть не один. Далее корректность работы алгоритма определяется подачей на вход слова некоторого тестового набора значений. Самое что трудное встречалось - верная(правильная) оптимизация приводила к искажению значений базовых адресов относительно которых считается смещение в памяти. Насчет баланса открывающих и закрывающих слов, типа BEGIN UNTIL и т.п., как быт елси мы вносим новую управляющую конструкцию на их основе? самое непонятное,- что делать c IMMEDIATE-словами?

ты не понял.
пишем, к примеру:
: something ( n n u addr --> addr u ) ... ;
слово собралось, стековая диаграмма запомнилась где-то в памяти отдельно от откомпилированного кода.
на этом этапе верификации нет, а стековая диаграмма в принципе может отсуствовать.
дальше пишешь:
' something verify
и тебе сообщают, что в одном из вариантов на ветвлении возвращается не addr u а addr u n - то есть не совпадают стековая диаграмма и то, что получается при исполнении.
второй момент, тебе сообщается, что внутри слова производится попытка сохранения значения не по адресу.
как миниму это уже было бы очень полезно.
понятно, что вычисление производится для всех слов, используемых в something
понятно, что будут неверифицируемые случаи, или частично верифицируемые: if execute then, тут придется либо верить приведенной стековой диаграмме.
такая вот идея

Не будет неувязок с CREATE ... DOES> конструкцией?

а почему они должны быть?
то есть понятно, что после DOES> должна быть стековая диаграмма, либо она должна будет вычисляться.
ведь в коде в CREATE части находится call на does> часть.

Ссылка немного в сторону от темы, но может быть пригодится… http://www.ict.nsc.ru/ws/YM2002/4760/