Семантика языка предикатного программирования P формализована с использованием трех видов отношений: совместимости, согласованности и тождества. Рекурсивные типы определены через аппарат наименьшей неподвижной точки. Обобщенные типы представлены типовыми ограничениями (концептами). Для конструкций с неявной типизацией сформулированы правила восстановления типов переменных. Разработаны алгоритмы проверки корректности рекурсии, определения типов для языковых конструкций, проверки семантической корректности конструкций.
Выполнен обзор работ, формирующих теоретические основы вычислений на сетях Слепцова и представляющих особенности рисования, компиляции и компоновки программ на языке сетей Слепцова, а также массово параллельные архитектуры вычисляющей памяти для реализации процессоров сетей Слецова. Сеть Петри выполняется экспоненциально медленнее и является частным случаем сети Слепцова. Рассмотрена универсальная сеть Слепцова, содержащая 13 позиций и 26 переходов, представляющая собой прототип процессора сетей Слепцова. Приведены примеры программ на языке сетей Слепцова для эффективного умножения, RSA шифрования/дешифрования, вычисления функции нечёткой логики и решения уравнения Лапласа. Преимуществами вычислений на сетях Слепцова являются наглядный графический язык, сохранение естественного параллелизма предметной области, мелкая грануляция параллельных вычислений, формальные методы верификации параллельных программ, быстрые массово-параллельные архитектуры, реализующие модель вычислений.
Описываются оптимизирующие трансформации для операций над списками и деревьями в системе предикатного программирования. Кодирование операций представлено набором правил, определяющих замену исходной операции на ее образ в императивном языке. Результатом трансформаций является императивная программа по эффективности сравнимая с написанной вручную.
В статье описывается структура онтологии шаблонов требований, извлекаемых из текстов технической документации. Эта онтология комбинирует шаблоны известных классификаций требований с новыми шаблонами. Язык онтологии допускает запись булевых комбинаций шаблонов следующих типов: качественных, реального и ветвящегося времени, с комбинированными событиями, количественными характеристиками событий и простыми утверждениями о данных. Приведены примеры шаблонов требований к реальной системе управления вакуумированием Большого солнечного вакуумного телескопа. Изложена схема интеллектуальной системы поддержки формальной верификации распределенных программных систем.
В статье предлагается понятие концептуальной модели языка программирования. Этот формализм представляет типы языка программирования, значения, исключения, состояния и выполнимые конструкции абстрактной машины языка программирования, и ограничения для этих сущностей на концептуальном уровне. Представляется новое определение концептуальных систем переходов, ориентированное на спецификацию концептуальных моделей языков программмирования, описывается язык переопределенных концептуальных систем переходов CTSL, и предлагается техника использования CTSL в качестве предметно-ориентированного языка спецификации концептуальных моделей языков программирования. Концептуальные модели для семейства простых языков программирования иллюстрируют эту технику.
В статье предлагается понятие концептуальной операционной семантики языка программирования. Этот формализм представляет операционную семантику языка программирования в терминах его концептуальной модели, основанной на концептуальных системах переходов. Определяется специальный вид концептуальных систем переходов - операционные концептуальные системы переходов, ориентированный на спецификацию концептуальной операционной семантики языков программирования, описывается расширение языка концептуальных систем переходов CTSL для операционных концептуальных систем переходов, и предлагается техника использования расширенного CTSL в качестве предметно-ориентированного языка спецификации концептуальной операционной семантики программных языков. Концептуальная операционная семантика для семейства модельных языков программирования иллюстрирует эту технику.