История изменений
Исправление SZT, (текущая версия) :
Для чего ты это (код на Си) написал? Тебе оно может и добавляет понимания, а мне - не добавляет.
А что должно добавить понимания?
Когда кто-то где-то упоминает о математической логике, значит в коде программы должны быть метаданные мегатоннами. И язык нужен соответствующий, с RTTI (например C++).
RTTI это про хранение типов в рантайме, к теории массивов и матлогике это отношения не имеет. Чтобы через теорию массивов что-то статически доказывать (см cтатический анализ кода) относительно свойств программы, никакое RTTI не требуется. Могут потребоваться специальные аннотации, типа ACSL https://frama-c.com/html/acsl.html но это не RTTI
Исправление SZT, :
Для чего ты это (код на Си) написал? Тебе оно может и добавляет понимания, а мне - не добавляет.
А что должно добавить понимания?
Когда кто-то где-то упоминает о математической логике, значит в коде программы должны быть метаданные мегатоннами. И язык нужен соответствующий, с RTTI (например C++).
RTTI это про хранение типов в рантайме, к теории массивов и матлогике это отношения не имеет. Чтобы через теорию массивов что-то статически доказывать относительно свойств программы, никакое RTTI не требуется. Могут потребоваться специальные аннотации, типа ACSL https://frama-c.com/html/acsl.html но это не RTTI
Исходная версия SZT, :
Для чего ты это (код на Си) написал? Тебе оно может и добавляет понимания, а мне - не добавляет.
А что должно добавить понимания?
Когда кто-то где-то упоминает о математической логике, значит в коде программы должны быть метаданные мегатоннами. И язык нужен соответствующий, с RTTI (например C++).
RTTI это про хранение типов в рантайме, к теории массивов и матлогике это отношения не имеет.