Статический анализ кода (на примере 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
(
@“from 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