Анализ структуры покрытий

Анализ структуры предопределенных покрытий

Во время работы тестовой системы может потребоваться отслеживать достижение различных ситуаций, определенных как элементы некоторого покрытия. Часть покрытий определяется явно при помощи указания способов определения того факта, реализовалась ли входящая в них ситуация, или нет. Часть покрытий вычисляется на основе операций над другими покрытиями. Здесь мы описываем третью часть, которая опеределяется неявно на основе операторов branch, mark и ветвлений в пред- и постусловиях.

Это 4 стандартных покрытия - функциональные ветви, маркированные пути, предикаты ветвлений и дизъюнкты. Далее определяется идентификация элементов разбиений по предикатам и дизъюнктам и строится таблица соответствия значений элементарных логических формул элементам 4-х стандартных покрытий, приводятся определения используемых терминов и алгоритм построения таблицы с примерами.

Существенным ветвлением называется разветвление потока управления в предусловии операции или постусловии операции, определяемое операторами if( ... ) { ... }, if( ... ) { ... } else { ... }, if( ... ) { ... } else if( ... ) { ... } else { ... } и пр., или switch( ... ) { ... }, имеющими в качестве условия или выражения выбора выражение, не являющееся константой, и не входящими в блок, помеченный как irrelevant, в блок одного их операторов try, catch или finally, или в цикл (такие блоки и циклы называем несущественными блоками).
Запрещено как-то прерывать поток выполнения от предусловия операции до операторов branch, или вторгаться в этот поток извне.
В частности,

• либо оператор branch, и причем ровно один, должен встречаться на каждом пути по графу потока управления от входа в постусловие до выхода из него
  либо операторов branch вообще нет в постусловии, при этом считается, что перед первой его инструкцией стоит
  branch SINGLE ;
• не должно быть недостижимых операторов branch
• идентификаторы, используемые в различных операторах branch внутри одного постусловия, должны быть разными
• оператор branch не может находиться внутри несущественного блока
• операторы return в предусловии не должны встречаться внутри несущественных блоков

• логическое выражение, не являющееся константой true или false и являющееся частью условия некоторого оператора if( ... ), определяющих существенное ветвление или значение возвращаемого выражения одного из операторов return в предусловии или постусловии операции, или полученное из выражений перечисленных видов с помощью приведенных ниже преобразований, и не разбиваемое на логические подвыражения, связанные логическими операторами (&&, ||, !, =>, &, |, ^, ==, !=, ?:).
  При определении элементарных формул выражение условия разбивается на логические подвыражения, связываемые перечисленными операторами до тех пор, пока это возможно, получаемые в результате выражения и являются элементарными формулами.
  При разборе логического выражения, имеющего в качестве оператора верхнего уровня оператор pre, этот оператор снимается, после чего полученное выражение анализируется дальше.
• "выражение" вида( Expression== $value ), где Expression - нелогическое выражение выбора в некотором операторе switch( ... ) существенного ветвления, $value - одно из возможных её значений, участвующих в case-метках внутри блока того же оператора switch( ... ).
• для каждогоSE_Access, указанного в последовательности с общим модификатором reads,"выражение" вида reads SE_Access.
  

• $x != $y ---> !( $x == $y )
• $x <= $y ---> !( $y < $x )
• $x > $y ---> $y < $x
• $x >= $y --->!( $x < $y )

• $x != $y ---> !( $x == $y )
• $x <= $y ---> !java.lang.Double.isNaN( $x ) && !java.lang.Double.isNaN( $y ) && !( $y< $x )
• $x > $y ---> $y < $x
• $x >= $y ---> !java.lang.Double.isNaN( $x ) && !java.lang.Double.isNaN( $y ) && !( $x < $y )

Заметим, что при этом могут появиться новые элементарные формулы вида java.lang.Double.IsNaN( $x) и java.lang.Float.IsNaN( $x).

После указанных преобразований элементарные формулы, отождествляются по текстуальному совпадению, за одним исключением - перед этим отождествлением локальным переменным, декларированным в пред- и постусловиях с одинаковыми именами, присваиваются различные имена, чтобы формулы с участием различных переменных не совпадали. Однако при подсчете дизъюнктов мы используем различные вхождения формул - здесь серьезное различие с подходами в предшествующих инструментах.
Это сделано для предотвращения пропуска некоторых путей при подсчете дизъюнктов из-за использования одной формулы несколько раз. Такой пропуск возникает, если перебирать значения формул так, как описано ниже, а совпадающие текстуально формулы помещать в таблицу только один раз.
Некоторые из них можно отождествить по текстуальному совпадению - это отождествление влияет на список элементарных формул в данном методе, заносимый в информацию о покрытиях, но не должно влиять на таблицу дизъюнктов - там все вхождения одной и той же формулы в код должны отражаться отдельно, в порядке их положения в коде.

Спецификация одной операции должна быть написаны таким образом, чтобы текстуально совпадающие элементарные формулы имели один и тот же смысл и одно и то же значение до предусловия, в предусловии и в постусловии до branch. Они могут поменять значение после branch.

Для устранения одной из вожможных ошибок можно запретить использование в совпадающих по тексту элементарных формулах различных локальных переменных.
Кроме того, как уже говорилось, локальные пременные пред- и постусловия считаются различными и текстуально одинаковые формулы, использующие одна - переменную из предусловия, другая - переменную из постусловия, считаются разными.

На структуру критериев покрытия влияют только некоторые элементарные формулы. Элементарные формулы, встречающиеся только в существенных ветвлениях, находящихся после операторов branch по потоку управления, в операторах return постусловия и формулы вида reads SE_Access, не влияют на определение покрытия (см. единственное исключение в точной формулировке алгоритма). Мы будем называть такие элементарные формулы несущественными.

Выражения, из которых построена элементарная формула при помощи операторов ==, !=, <=, >=, <, >, и пр., будем называть термами.

Дизъюнктом далее называется набор значений некоторого подмножества элементарных формул, однозначно определяющий путь по графу потока управления (построенного только с учётом существенных ветвлений) предусловия операции и постусловия той же операции до одного из операторов branch (если в постусловии есть хотя бы один, иначе постусловие не учитывается) и положительный результат предусловия, при этом содержащий минимальное число элементарных формул, т.е., из множества элементарных формул, имеющих значения в рамках определяющего дизъюнкта, ни одну нельзя перевести в разряд не имеющих значение так, чтобы полученное множество значений элементарных формул однознозначно определяло указанные путь и результат предусловия.
При этом считается, что элементарная формула использовалась при вычиселнии пути по графу, если при вычислении этого пути использовалось хотя бы одно вхождение этой формулы.
Если в пред- и постусловии нет существенных элементарных формул, то считаем, что единственный имеющийся путь соответствует специальному дизъюнкту true.

Предикатом (пока речь идет о покрытиях) называется логическое выражение, значение которого определяет существенное ветвление в графе потока управления пред- или пост- условия.

При построении предикатов рассматриваются существенные операторы if( ... ) и switch( ... ) такие что

• они находятся в предусловии или в постусловии операции до одного из операторов branch по потоку управления,
• выражения в круглых скобках не являются константами, вычислимысм на стадии компиляции.

Для оператора if( ... ) строятся два предиката.:

1. условие if. Определяет переход на then-часть оператора if.
2. отрицание этого условия. Определяет переход на else-часть оператора if или, если else не было, - на конечную точку if.

Для оператора switch( ... ) по выражением $variable (находящегося там же) предикаты строятся по следующим правилам. Метки (case и default), между которыми нет StatementSwitchElement, будем называть смежными метками.
Набор смежных между собой меток будем называть блоком смежных меток.
Предикат не строится, если

• switch не содержит ни одного элемента;
• switch содержит только один блок смежных меток, и в этом блоке есть default

• для каждого блока смежных меток, не содержащего default, строится предикат - дизъюнкция элем. формул всех меток этого блока: ( $variable == $value_1 ) || ...|| ( $variable == $value_m ).
  сюда же относится случай отдельно стоящей case-метки (то есть не смежной ни с какой другой меткой).
• для блока меток, содержащего default, строится предикат - конъюнкия отрицаний элем. формул всех меток, не входящих в этот блок: !( $variable == $value_1 ) && ...&& !( $variable == $value_k )
  таким образом, метки, смежные с default, не участвуют в построении предикатов.
• если switch не содержит default, то строится предикат того же вида, что и в предыдущем случае, только конъюнкция ведётся по элементарным формулам всех меток switch.

{ 
    pre
    {
        if( !a && b )
        {
            mark "1";
            return true;
        }
        else return x;
    }
    post
    {
        if( !a && b && !x )
        {
            if( g(m) == 17 ) mark "2";
            branch B1;
            return ( g(m) - 17 ) >= 0;
        }
        else if( m != 0 )
        {
            branch B2;
            return x != a;
        }
        else
        {
            if( k > 5 )
            {
                if(!x) {...}
                branch B3;
                return f(a);
            }
            else
            {
                switch(k)
                {
                    case 4: mark "3"; break;
                    case 3: case2: ...; break;
                    default: ...;
                }
                branch B4;
                return true;
            }
        }
  } 
}

1. Находим все существенные элементарные формулы.
   Для этого в предусловии операции и её постусловии выделяются все существенные ветвления, находящиеся до операторов branch, определяются соответствующие определяющие предикаты и элементарные формулы.
   Кроме того, существенные элементарные формулы выделяются из выражений, стоящих в операторах return, находящихся в предусловиях.
   Далее в описании алгоритма элементарными формулами называются только существенные, соответственно, вхождениями элементарных формул - только существенные вхождения.
   Для всех определяющих предикатов генерируются числовые идентификаторы (#PID( $predicate ), например, если предикаты просто перенумеровать в порядке нахождения в коде), кроме того запоминается их логическое представление.
2. Для того, чтобы сделать более эффективным учёт естественных тавтологий определённого вида, выделенные элементарные формулы приводятся к канонической форме, а именно, по указанным выше правилам

• Имена типов, используемые в формулах, заменяются на полные имена соответсвующих типов
• Формулы освобождаются от внешних скобок
• Сравнения числовых типов преобразуются по указанным выше правилам так, чтобы остались только формулы, содержащие в качестве внешней операции == и <. При этом элементарные формулы анализируются только до определения внешней операции, а их термы отождествляются по текстуальному совпадению
• Для всех полученных элементарных формул (на предыдущем шаге могут добавиться новые элементарные формулы), с точностьб до текстуального совпадаения, генерируются числовые идентификаторы #FID( $formula ), кроме того, запоминается строка, совпадающая с текстовым представлением элементарной формулы. Т.е. идентификатор генерируется один раз для формулы, даже если она встречается в коде несколько раз.

• На множестве вхождений элементарных формул в код вводится линейный порядок, совпадающий с порядком их использования в коде пред- и постусловий, т.е., формула, которая в тексте спецификации встречается раньше, должна быть ближе к началу и в определяемом порядке. Далее для удобства считаем, что формируется список вхождений элементарных формул.
  Формула с одним идентификатором может встречаться в этом порядке на нескольких местах, соответственно ее вхождениям в код.
  Формулы, используемые только после операторов branch или имеющие вид reads $x идут после всех остальных и не учитываются.
• Собственно построение таблицы соответствий - перебираются наборы значений вхождений элементарных формул, для каждого набора делается проход по предусловию операции и её постусловию до первого оператора branch, при этом определяется, значения каких вхождений формул использовались, какие последовательности предикатов и марок были пройдены, какой идентификатор branch соответствует данному проходу.
  Точнее

1. В самом начале, до первого шага, набор значений вхождений элементарных формул выглядит так: (false, ... , false). Все вхождения считаются несущественными.
   
2. Шаг: В начале каждого шага проверяется выполнение примитивных тавтологий.
   Если на текущем наборе значений вхождений элементарных формул все вхождения каждой элементарной формулы имеют одно и то же значение, переходим к шагу 3.
   Иначе ищем множество смежных несовместных вхождений D. Смежными несовместными вхождениями элементарной формулы ef называется пара её вхождений ( i , j ), имеющих различные значения, и между которыми нет других вхождений ef.
   Поиск элементов D проводится по списку вхождений элементарных формул слева направо.
   Считаем использованными при обсчёте примитивных тавтологий вхождения с номерами i и j такие, что ( i , j ) принадлежит D, и j имеет минимальное значение среди правых частей пар множества D.
   Переходим к п. 6.
3. Далее проверяется выполнение естественных тавтологий и тавтологий, указанных в операторах tautology. Если значение хотя бы одной из тавтологий оказывается равно false, - переходим к п. 6.
   
4. Делаем проход по предусловию операции, используя имеющийся набор значений вхождений формул, запоминаем множество вхождений, использованных при вычислении условий существенных ветвлений при данном проходе (попадание на некоторую ветку оператора switch( ... ) считается использованием формул вида( $variable == $value ), входящих в соответствующий этой ветке предикат). Так же запоминаем
   • последовательность идентификаторов предикатов, через которые прошло управление при данном проходе
   • последовательность строковых литералов в пройденных операторах mark

   Если результат предусловия равен false, забываем запомненные последовательности и переходим к п. 6.

5. Если в постусловии есть хотя бы один оператор branch, делаем проход по постусловию операции до первого встретившегося оператора branch, используя имеющийся набор значений вхождений элементарных формул, запоминаем множество вхождений, использованных при вычислении условий существенных ветвлений при данном проходе. Попадание на некоторую ветку оператора switch( ... ) считается использованием всех формул вида( $variable == $value ), входящих в соответствующий этой ветке предикат а так же в предикаты, порождённые предшествующими ветками того же switch, за исключением default-ветки.
   После этого добавляем в конец запомненных на предыдущем шаге последовательностей
   • последовательность идентификаторов предикатов, через которые прошло управление при данном проходе
   • последовательность строковых литералов в пройденных операторах mark и идентификатор branch
   • запоминаем отдельно идентификатор ветви в операторе branch

   Если в постусловии нет операторов branch, или не было самого постусловия, сразу добавляем в конец последовательности строковых литералов в пройденных операторах mark идентификатор ветви Single.

   После заносим полученный дизъюнкт (набор true, false и неиспользованных формул) в таблицу. При занесении дизъюнкта в таблицу строим его идентификатор (например, номер), и заносим в таблицу, что он соответствует

   • Запомненной последовательности идентификаторов предикатов - полному предикату.
     Для этой последовательности определяем уникальный номер и строковое представление.
   • Запомненной последовательности строк в операторах mark и branch.
     Для этой последовательности определяем уникальный номер и строковое представление.
   • Функциональной ветви, определяемой оператором branch
   (или, если таких операторов нет, единственной ветви с идентификатором Single) .
   Для этой ветви определяем уникальный номер и строковое представление, совпадающее с идентификатором.
   
6. Здесь мы поступаем по разному, в зависимости от того, откуда мы попали на этот шаг.
   
   • Если на этом шаге мы оказались после шага 4 или 5, то смотрим на использованные вхождения.
     
     • Если значения всех использованных вхождений равны true, переходим к п. 7.
     • Иначе, меняем значение последнего в выбранном порядке использованного вхождения, равного false, на true, а значения всех вхождений, следующих в выбранном порядке за ним, приравниваем false.
       Объявляем все вхождения неиспользованными и переходим к п. 2.
   • Если мы попали на этот шаг сразу после шага 2 или 3, то поступаем так.
     Пусть $rightmost_used - самое правое вхождение элементарной формулы, использованное при подсчёте нарушившейся тавтологии.
     
     • Если значения $rightmost_used и всех вхождений, предшествующих $rightmost_used, равны true, то переходим к п. 7.
     • Иначе, ищем последнее (крайнее правое) предшествующее $rightmost_used (или совпадающее с ним) вхождение, значение которого равно false. Меняем значение этого найденного вхождения на true, а значения всех следующих за ним вхожедний устанавливаем в false. Переходим к п. 2.
7. Конец построения таблицы соответствий.

Определим теперь, какое подмножество естественных тавтологий инструмент мог бы отслеживать.

• В первую очередь, это тавтологии, связанные со свойствами равенства на объектах, перечислимых и встроенных типах, а именно
  ( $x== $y ) => ( $y == $x ), ( $x == $y ) && ( $y == $z ) => ( $x == $z )
  
• Следующие - тавтологии переноса равенства на свойства равных объектов.
  Для всех полей a, декларированных в наиболее узком общем типе объектов $x и $y, ( $x == $y ) => ( $x.a == $y.a ).
  Аналогично, для всех вызовов метода m(x1,..., xn) с одинаковыми выражениями в качестве параметров в наиболее узком общем типе объектов $x и $y, ( $x == $y ) => ( $x.m(x1,..., xn) == $y.m(x1,..., xn) ).
  
• Далее идут тавтологии, связанные со свойствами порядка на перечислимых и встроенных числовых типах.
  Для таких тавтологий и тавтологий равенства у Сережи Зеленова есть алгоритм проверки, основанный на построении графа отношений между различными термами, входящими в элементарные формулы. В этом графе отношения равенства, неравенства и порядка представляются по-разному помеченными ребрами между вершинами, соответсвующими термам. Проверка происходит путем стягивания вершин, соединенных отношениями равенства, и циклов вершин по отношению >= (отрицание <). После чего можно искать петли-неравенства. Такая петля означает нарушение естественных тавтологий, связанных с порядком и равенством.
  Можно пополнить алгоритм, отмечая вершины, соответствующие термам-константам, значение которых известно во время компиляции. Для таких термов можно добавить дополнительные неравенства между разными константами и равенства между одинаковыми.
  Для отвергнутых согласно таким тавтологиям наборам значений формул существенные формулы нужно определять так: раскрываем обратно стянутые по равенствам и циклам из >= вершины, при этом петля по неравенству соответсвует циклу, содержащему неравенство и несколько дуг, соответсвующих равенствам и >=. Все формулы, входящие в этот цикл надо считать существенными.
  Надо отметить, что для типов float и double есть особенности, связанные с наличием значения NaN. Если выполнено свойство java.lang.Double.IsNaN( $x ), то для всякого $y выполнено !( $x == $y ) и !( $x < $y ) и !( $y < $x ). Приведенный алгоритм нужно пополнить отметками на вершинах, термы которых имеют значение NaN. Тогда любое сравнение по порядку или равенство такой вершины с любой другой означает нарушение ествественных тавтологий.
  
• Следующий шаг - обнаружение естественных тавтологий вида ![ ( 1 < $x ) && ( $x < 2 ) ] для целочисленного $x.
  Для этого в построенном ранее графе для целочисленных термов с вершинами-константами надо искать наиболее длинные пути по неравным вершинам от одной константы к другой. Если число вершин на таком пути больше или равно разности между константами, это является нарушением свойств порядка на целых числах. Если же на всех путях число вершин меньше разности между константами, можно подобрать такие значения термов, что все соотноения порядка и неравенства будут выполнены.
  Аналогично можно работать и для типов float, double и decimal, с той лишь разницей, что вместо разности между константами нужно брать число значений данного типа между этими константами плюс 1.