Статический анализ кода (на примере DDD-фреймворка) Алексеев Алексей alekseev.aleksei@gmail.com aalekseev@custis.ru Николай Гребнев ngrebnev@gmail.com. - презентация

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

18 Запросы к доменной модели На языке 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;

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

20 Требуется: Но в 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;

21 Свойства, используемые в запросах В 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(); 0; } } … } … var q = from Employee e in Session.Employee where e.IsManager select e; q.ToList();">

22 Решение 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();

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

24 Корректность [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; } }

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

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

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

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

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

30 Декларативные ограничения [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() {...}

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

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

33

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

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

36 CTL

37

38

39

40

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