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

Содержание

1. Статический анализ кода (на примере DDD-фреймворка)
2. Структура доклада Введение Статические проверки DDD-фреймворк Поддержка LINQ Модель состояний Верификация модели состояний
3. Структура доклада Введение Статические проверки DDD-фреймворк Поддержка LINQ Модель состояний Верификация модели состояний
4. Человеческий фактор
5. Общепринятые методологии Ручное тестирование Автоматическое тестирование, TDD Code Review
6. Средства разработки
7. Структура доклада Введение Статические проверки ДДД-фреймворк Поддержка LINQ Модель состояний Верификация модели состояний
8. Стоимость исправления ошибок Момент выявления ошибки:
9. До написания кода Статические проверки
10. Аспекты статических проверок Диагностика Скорость Полнота
11. Полнота статических проверок С++: if (a =
12. Структура доклада Введение Статические проверки DDD-фреймворк Поддержка LINQ Модель состояний Верификация модели состояний
13. Терминология ORM – object relational mapper: Отображение:
14. ВАЛИДАЦИЯ МОДЕЛИ ВО ВРЕМЯ КОМПИЛЯЦИИ Демонстрация
15. Статическая проверка метамодели
16. Структура доклада Введение Статические проверки DDD-фреймворк Поддержка LINQ Модель состояний Верификация модели состояний
17. ПОДДЕРЖКА LINQ Полнота поддержки LINQ напрямую влияет на снижение влияния человеческого фактора в разработке ПО
18. Запросы к доменной модели На языке ORM:
19. Преимущества LINQ Статическая типизация IntelliSense Полная интеграция в язык программирования
20. Требуется: Но в Entity
21. Свойства, используемые в запросах В Entity Framework:
22. Решение public class Employee {
23. from Employee e in Session select e.IsManager
24. Корректность [Attr] [Implemented] public abstract MyEntity
25. Пример анализа реализации static Expression
26. Структура доклада Введение Статические проверки Валидация модели
27. Состояния /// Состояние автомобиля. [Flags]
28. Императивные проверки [Method] public virtual void WindUp()
29. Декларативные ограничения [Method] [StateRestriction(AutoState.Stopped)] public virtual void
30. Декларативные ограничения [Method] [StateRestriction(AutoState.Stopped)] [StateTransition(AutoState.Stopped,
31. Структура доклада Введение Статические проверки Валидация модели
32. Структура Крипке
33. Структура Крипке
34. CTL, формулы состояний CTL - Computation tree
35. CTL, формулы пути Формулы пути: X
36. CTL
41. Список литературы Ю.Г. Карпов. Model Checking. Верификация

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

Главная
Разное
Статический анализ кода (на примере 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 q =
new

SimpleQuery(
@“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();

0; } } …}…var q = from Employee e in Session.Employee where e.IsManager select e;q.ToList();">

Свойства, используемые в запросахВ Entity Framework:Указанный член типа

Слайд 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();

Слайд 23from 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Структура Крипке

Слайд 34CTL, формулы состояний
CTL - Computation tree logic.
Формулы состояний:
A f -

All: f должен выполняться на всех путях из данного состояния;
E f - Exists: существует хотя бы один путь из данного состояния, на котором выполняется f.

В этом определении f – формула пути.

Слайд 35CTL, формулы пути
Формулы пути:
X p - Next: p выполняется на

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

Слайд 36CTL

Слайд 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.http://www.introducinglinq.com/files/folders/5/download.aspx http://www.introducinglinq.com/files/folders/5/download.aspx LINQ introduction.
http://www.rsdn.ru/article/design/Code_Contracts.xml Проектирование по контракту.

Скачать презентацию

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

Содержание

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

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

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

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

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

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

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

Слайд 8Стоимость исправления ошибокМомент выявления ошибки: До написания кода Статические проверки Unit-тесты

Слайд 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

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

Слайд 20Требуется:Но в Entity Framework:Не удалось создать константу с типом "Тип замыкания".

Слайд 21Свойства, используемые в запросахВ Entity Framework:Указанный член типа "IsManager" не поддерживается

Слайд 22Решениеpublic class Employee{ … [Attr] [Implemented] public

Слайд 23from Employee e in Sessionselect e.IsManagerСвойства, используемые в запросахfrom Employee e

Слайд 24Корректность [Attr][Implemented]public abstract MyEntity Attr1 {get; } [Attr][Implemented]public abstract MyEntity

Слайд 25Пример анализа реализацииstatic Expression Attr1Impl{ get {return e

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

Слайд 27Состояния/// Состояние автомобиля. [Flags][State]public enum AutoState{ /// Машина

Слайд 28Императивные проверки[Method]public virtual void WindUp(){ if (State != AutoState.Stopped)

Слайд 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,

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