'

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

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





Слайд 0

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


Слайд 1

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


Слайд 2

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


Слайд 3

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


Слайд 4

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


Слайд 5

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


Слайд 6

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


Слайд 7

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


Слайд 8

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


Слайд 9

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


Слайд 10

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


Слайд 11

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


Слайд 12

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


Слайд 13

Валидация модели во время компиляции Демонстрация


Слайд 14

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


Слайд 15

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


Слайд 16

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


Слайд 17

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


Слайд 18

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


Слайд 19

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


Слайд 20

Свойства, используемые в запросах В 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();


Слайд 21

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


Слайд 22

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


Слайд 23

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


Слайд 24

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


Слайд 25

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


Слайд 26

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


Слайд 27

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


Слайд 28

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


Слайд 29

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


Слайд 30

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


Слайд 31

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


Слайд 32

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


Слайд 33

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


Слайд 34

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


Слайд 35

CTL


Слайд 36


Слайд 37


Слайд 38


Слайд 39


Слайд 40

Список литературы Ю.Г. Карпов. 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:





Ссылка: