ВПнМ, примеры задач/Задача 1

Материал из eSyr's wiki.

Версия от 23:59, 24 апреля 2008; ESyr01 (Обсуждение | вклад)
(разн.) ← Предыдущая | Текущая версия (разн.) | Следующая → (разн.)
Перейти к: навигация, поиск

Содержание

[править] Задание

Будем считать состоянием модели значение счётчика команд (неявная переменная потока управления) и значения всех переменных заданной программы. Требуется:

  1. Оценить размер множества потенциальных состояний программы. Ответ обосновать. В обосновании описать множество потенциальных состояний.
  2. Оценить размер множества достижимых состояний программы. Ответ обосновать. В обосновании описать множество достижимых состояний.
  3. Построить LTS для значений параметра a = 1, b = 2, c =3. Описание LTS может быть как текстовым, так и графическим (например, выполненным при помощи средства GraphViz, http://www.graphviz.org).

[править] Вариант 1

void
f (int a, int b, int c)
{
 int x = 0, y = 0, z = 0;
 x = 4;
 y = 1;
 z = a;
 if (y > 6)
   {
    x = 2;
     z = y + x;
     if (z > c)
       {
         x = 10;
       }
     if (y > 6)
       {
          z = b;
       }
     else
       {
         x = 5;
       }
     y = 2;
     y = 2;
   }
 y = 2;
}

[править] Решение

[править] Количество потенциальных состояний

    void
    f (int a, int b, int c)
    {
 0: 	int x = 0, y = 0, z = 0;
 1: 	x = 4;
 2: 	y = 1;
 3: 	z = a;
 4: 	if (y > 6)
    	{
 5: 		x = 2;
 6: 		z = y + x;
 7: 		if (z > c)
    		{
 8: 			x = 10;
    		}
 9: 		if (y > 6)
    		{
10: 			z = b;
    		}
    		else
    		{
11: 			x = 5;
    		}
12: 		y = 2;
13: 		y = 2;
    	}
14: 	y = 2;
    }

Количество потенциальных состояний (сумма состояний для каждого оператора, всего переменных 6 в каждой точке программы, для каждой 2^32 вариантов): 15 * 2^(32 * 6)


[править] Количество достижимых состояний

                                     a       b       c       x       y       z
    void                           
    f (int a, int b, int c)
    {                              
 0:     int x = 0, y = 0, z = 0;   2^32    2^32    2^32      1       1       1
 1:     x = 4;                     2^32    2^32    2^32      1       1       1
 2:     y = 1;                     2^32    2^32    2^32      1       1       1
 3:     z = a;                     2^32    2^32    2^32      1       1     2^32
 4:     if (y > 6)                 2^32    2^32    2^32      1       1     2^32
        {                          
 5:         x = 2;                   0       0       0       0       0       0
 6:         z = y + x;               0       0       0       0       0       0
 7:         if (z > c)               0       0       0       0       0       0
            {                      
 8:             x = 10;              0       0       0       0       0       0
            }                      
 9:         if (y > 6)               0       0       0       0       0       0
            {                      
10:             z = b;               0       0       0       0       0       0
            }                      
            else                   
            {                      
11:             x = 5;               0       0       0       0       0       0
            }                      
12:         y = 2;                   0       0       0       0       0       0
13:         y = 2;                   0       0       0       0       0       0
        }                          
14:     y = 2;                     2^32    2^32    2^32      1       1     2^32
    }                              

Количество достижимых состояний для программы — сумма количества достижимых состояний для каждой точки программы, что, в свою очередь — произведение количество состояний переменных в данной точке. Итого: (2^96 + 2^128) * 3.

[править] LTS

PNG, полученный из сгенерированного SVG
PNG, полученный из сгенерированного SVG
digraph LTS1 {
	0 [label="0 (1, 2, 3, 0, 0, 0)"];
	1 [label="1 (1, 2, 3, 4, 0, 0)"];
	2 [label="2 (1, 2, 3, 4, 1, 0)"];
	3 [label="3 (1, 2, 3, 4, 1, 1)"];
	4 [label="4 (1, 2, 3, 4, 1, 1)"];
	14 [label="14 (1, 2, 3, 4, 2, 1)"];
 
	0 -> 1 -> 2 -> 3 -> 4 -> 14;
}

Команда сборки диаграммы:

dot -Tsvg -o"LTS1.svg" -Kdot LTS1.dot


Верификация программ на моделях


01 02 03 04 05 06 07 08 09 10


Календарь

пт пт пт пт пт
Февраль
  08 15 22 29
Март
  14 21 28
Апрель
04 11 18

Материалы по курсу
Список вопросов к экзамену | Примеры задач: 1 2 3 4 5 | Теормин

Личные инструменты
Разделы