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

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

(Различия между версиями)
Перейти к: навигация, поиск
(Новая: == Задание == Будем считать состоянием модели значение счётчика команд (неявная переменная потока упра...)
м
Строка 105: Строка 105:
==== LTS ====
==== LTS ====
-
[[Image:LTS1.png|thumb]]
+
[[Image:LTS1.png|thumb|PNG, полученный из сгенерированного SVG]]
digraph LTS1 {
digraph LTS1 {
Строка 117: Строка 117:
0 -> 1 -> 2 -> 3 -> 4 -> 14;
0 -> 1 -> 2 -> 3 -> 4 -> 14;
}
}
 +
 +
Команда сборки диаграммы:
 +
dot -Tsvg -o"LTS1.svg" -Kdot LTS1.dot
{{Курс ВПнМ}}
{{Курс ВПнМ}}

Версия 23:42, 24 апреля 2008

Содержание

Задание

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

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

Варианты

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 | Теормин

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