Статический анализ кода (на примере DDD-фреймворка) Алексеев Алексей Николай Гребнев

Структура доклада Введение Статические проверки DDD-фреймворк Поддержка LINQ Модель состояний Верификация модели состояний

Структура доклада Введение Статические проверки DDD-фреймворк Поддержка LINQ Модель состояний Верификация модели состояний

Человеческий фактор

Общепринятые методологии Ручное тестирование Автоматическое тестирование, TDD Code Review

Средства разработки

Структура доклада Введение Статические проверки ДДД-фреймворк Поддержка LINQ Модель состояний Верификация модели состояний

Стоимость исправления ошибок Момент выявления ошибки: До написания кода Статические проверки Unit-тесты Code Review Интеграционные тесты Ручные тесты Ошибка при эксплуатации Цена

До написания кода Статические проверки Unit-тесты Code Review Интеграционные тесты Ручные тесты Ошибка при эксплуатации Стоимость исправления ошибок Время выявления ошибки: Цена

Аспекты статических проверок Диагностика Скорость Полнота

Полнота статических проверок С++: if (a = 2) if (ptr == null) Корректность if (ptr) Лаконичность VS

Структура доклада Введение Статические проверки DDD-фреймворк Поддержка LINQ Модель состояний Верификация модели состояний

Терминология ORM – object relational mapper: – Отображение: Класс таблица Объект запись Свойство колонка – Запросы – Процесс компиляции

ВАЛИДАЦИЯ МОДЕЛИ ВО ВРЕМЯ КОМПИЛЯЦИИ Демонстрация

Статическая проверка метамодели

Структура доклада Введение Статические проверки DDD-фреймворк Поддержка LINQ Модель состояний Верификация модели состояний

ПОДДЕРЖКА LINQ Полнота поддержки LINQ напрямую влияет на снижение влияния человеческого фактора в разработке ПО

Запросы к доменной модели На языке ORM: LINQ: SimpleQuery q = new SimpleQuery Post p where p.Blog.Author = ?", author); return q.Execute(); from Post p in Session.Posts where p.Blog.Author == author select p;

Преимущества LINQ Статическая типизация IntelliSense Полная интеграция в язык программирования

Требуется: Но в Entity Framework: Не удалось создать константу с типом "Тип замыкания". В этом контексте поддерживаются только типы-примитивы ("например Int32, String и Guid"). Максимальная типизация в Linq Employee leader = Session.Employee.First(); var q = from Department d in Session.Department where d.Leader == leader select d;

Свойства, используемые в запросах В Entity Framework: Указанный член типа "IsManager" не поддерживается в выражениях LINQ to Entities. Поддерживаются только инициализаторы, члены сущности и свойства навигации сущности. public class Employee { … public bool IsManager { get { return Subordinates.Count() > 0; } } … } … var q = from Employee e in Session.Employee where e.IsManager select e; q.ToList();

Решение public class Employee { … [Attr] [Implemented] public abstract bool IsManager {get; } // Это реализация для атрибута IsManager. static Expression > IsManagerImpl { get { return e => Subordinates.Count() > 0; } } … } … var q = from Employee e in Session.Employee where e.IsManager select e; q.ToList();

from Employee e in Session select e.IsManager Свойства, используемые в запросах from Employee e in Session select Subordinates.Count() > 0

Корректность [Attr] [Implemented] public abstract MyEntity Attr1 {get; } [Attr] [Implemented] public abstract MyEntity Attr2 {get; } static Expression > Attr1Impl { get {return e => e.Attr2; } } static Expression > Attr2Impl { get {return e => e.Attr1; } }

Пример анализа реализации static Expression > Attr1Impl { get {return e => e.Attr2; } } static Expression > Attr2Impl { get {return e => e.Attr1; } } Обнаружена циклическая зависимость

Структура доклада Введение Статические проверки Валидация модели во время компиляции Поддержка LINQ Модель состояний Верификация модели состояний

Состояния /// Состояние автомобиля. [Flags] [State] public enum AutoState { /// Машина стоит и не заведена. Stopped = 1, /// Машина заведена и не едет. Winded = 2, /// Машина едет. Driving = 4, }

Императивные проверки [Method] public virtual void WindUp() { if (State != AutoState.Stopped) throw new InvalidEntityStateException(...);... } [Method] public virtual bool TryRun() { if (State != AutoState.Winded) throw new InvalidEntityStateException(...);... }

Декларативные ограничения [Method] [StateRestriction(AutoState.Stopped)] public virtual void WindUp() {...} [Method] [StateRestriction(AutoState.Winded)] public virtual bool TryRun() {...}

Декларативные ограничения [Method] [StateRestriction(AutoState.Stopped)] [StateTransition(AutoState.Stopped, AutoState.Stopped | AutoState.Winded)] public virtual void WindUp() {...} [Method] [StateRestriction(AutoState.Winded)] [StateTransition(AutoState.Winded, AutoState.Driving | AutoState.Stopped)] public virtual bool TryRun() {...}

Структура доклада Введение Статические проверки Валидация модели во время компиляции Поддержка LINQ Модель состояний Верификация модели состояний

Структура Крипке

CTL, формулы состояний CTL - Computation tree logic. Формулы состояний: – A f - All: f должен выполняться на всех путях из данного состояния; – E f - Exists: существует хотя бы один путь из данного состояния, на котором выполняется f. В этом определении f – формула пути.

CTL, формулы пути Формулы пути: – X p - Next: p выполняется на следующем состоянии пути; – G p - Globally: p выполняется на всех последующих состояниях пути; – F p - Finally p выполняется на одном из последующих состояний пути; – p U q - Until: p выполняется, пока на каком-то из состояний пути не выполнится q, причем q должен обязательно когда-нибудь выполнится в будущем. – p – формула состояния или предикат

CTL

Список литературы Ю.Г. Карпов. Model Checking. Верификация параллельных и распределенных программных систем. Turing award. Model Checking: Algorithmic Verification and Debugging. LINQ introduction. Проектирование по контракту.