'

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

Понравилась презентация – покажи это...





Слайд 1

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


Слайд 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<Post> q = new SimpleQuery<Post>( @“from 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();


Слайд 22

Решение public class Employee { … [Attr] [Implemented] public abstract bool IsManager {get; } // Это реализация для атрибута IsManager. static Expression<Func<Employee, bool>> 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<Func<MyEntity, MyEntity>> Attr1Impl { get {return e => e.Attr2; } } static Expression<Func<MyEntity, MyEntity>> Attr2Impl { get {return e => e.Attr1; } }


Слайд 25

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


Слайд 26

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


Слайд 27

Состояния /// <summary> Состояние автомобиля. </summary> [Flags] [State] public enum AutoState { /// <summary> Машина стоит и не заведена. </summary> Stopped = 1, /// <summary> Машина заведена и не едет. </summary> Winded = 2, /// <summary> Машина едет. </summary> 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. Верификация параллельных и распределенных программных систем. http://www-verimag.imag.fr/~sifakis/TuringAwardPaper-Apr14.pdf Turing award. Model Checking: Algorithmic Verification and Debugging. http://www.introducinglinq.com/files/folders/5/download.aspx LINQ introduction. http://www.rsdn.ru/article/design/Code_Contracts.xml Проектирование по контракту.


×

HTML:





Ссылка: