solution (Задание 1)
Описание файла
Файл "solution" внутри архива находится в следующих папках: Задание 1, Reliability_Task1 (answer) (UTF-8). Текстовый-файл из архива "Задание 1", который расположен в категории "". Всё это находится в предмете "надёжность программного обеспечения" из 7 семестр, которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр текстового-файла онлайн
Василенко Анатолий
421 группа
//====================================== ======================================== ======================================== ===============================
//====================================== ======================================== ======================================== ===============================
//====================================== ======================================== ======================================== ===============================
1 часть задания:
/////////////////////////
количество переменных - h, f_a, f_b, f_x, f_y, g_a, g_b, g_x, g_y - 9 штук
переменные размерности int, что значит, что каждая переменная может принимать 2^32 различных значений
операторы пронумерованны ниже:
/////////////////////////
int h;
void f (int a, int b)
{
0: int x, y;
1: x = 9;
2: y = 3;
3: h = 3;
4: h = a + y;
5: if (y > 6)
{
6: if (x > 9)
{
7: y = 4;
}
8: if (h < a + x)
{
9: h = y;
}
10: x = 5;
}
11: } // заключительный оператор
// Всего 12 операторов
void g (int a, int b)
{
0: int x, y;
1: x = 2;
2: y = 7;
3: h = 5;
4: x = 4;
5: h = b;
6: if (h < y)
{
7: y = 0;
}
else
{
8: x = 3;
}
9: while (x > 4)
{
10: if (h > 0)
11: break;
12: x = 1;
13: if (x > 5)
{
14: y = 6;
}
15: h = y;
}
16:} // Заключительное состояние
// Всего 17 операторов
/////////////////////////
Это означает, что количество потенциальных состояний программы = 12*17*(2^(32*9)) = 204*2^(288)
(Без учёта недостижимости)
Ответ: 12*17*(2^(32*9)) = 204 * 2^288
//====================================== ======================================== ======================================== ===============================
//====================================== ======================================== ======================================== ===============================
//====================================== ======================================== ======================================== ===============================
2 часть задания:
Проверим всё на достижимость:
/////////////////////////
// исходя из функции g - h на входе может быть равна {#} или {5, g_b, g_y}, причём т.к. функции выполняются параллельно и мы не знаем времени присваивания h в фукнции g, то придётся всё время считать, что h может быть изменено на {5, g_b, g_y}
int h;
void f (int a, int b)
{
0: int x, y; // h = {#, 5, g_b, g_y}; (-2^31 <= f_a <= 2^31 -1); (-2^31 <= f_b <= 2^31 -1)
1: x = 9; // h = {#, 5, g_b, g_y}; (-2^31 <= f_a <= 2^31 -1); (-2^31 <= f_b <= 2^31 -1); f_x = {#}; f_y = {#}
2: y = 3; // h = {#, 5, g_b, g_y}; (-2^31 <= f_a <= 2^31 -1); (-2^31 <= f_b <= 2^31 -1); f_x = {9}; f_y = {#}
3: h = 3; // h = {#, 5, g_b, g_y}; (-2^31 <= f_a <= 2^31 -1); (-2^31 <= f_b <= 2^31 -1); f_x = {9}; f_y = {3}
4: h = a + y; // h = {3, 5, g_b, g_y}; (-2^31 <= f_a <= 2^31 -1); (-2^31 <= f_b <= 2^31 -1); f_x = {9}; f_y = {3}
5: if (y > 6) // h = {f_a+f_y = f_a+3, 5, g_b, g_y}; (-2^31 <= f_a <= 2^31 -1); (-2^31 <= f_b <= 2^31 -1); f_x = {9}; f_y = {3}
{ // недостижимо, т.к. в условии стоит y > 6 , в то время, как f_y = {3}
6: if (x > 9) // недостижимо
{ // недостижимо
7: y = 4; // недостижимо
} // недостижимо
8: if (h < a + x) // недостижимо
{ // недостижимо
9: h = y; // недостижимо
} // недостижимо
10: x = 5; // недостижимо
} // недостижимо
11: } // заключительный оператор
// h = {f_a+3, 5, g_b, g_y}; (-2^31 <= f_a <= 2^31 -1); (-2^31 <= f_b <= 2^31 -1); f_x = {9}; f_y = {3}
// Исходя из уже проанализированной функции f (т.е. за вычетом недостижимых участков) - h на входе может быть равна {#} или {f_a+3, 3, f_y} (f_y - тоже, потому что недостижимость будет учтена позже на следующем раунде), причём т.к. функции выполняются параллельно и мы не знаем времени присваивания h в фукнции f, то придётся всё время считать, что h может быть изменено на {f_a+3, 3, f_y}
void g (int a, int b)
{
0: int x, y; // h = {#, f_a+3, 3, f_y}; (-2^31 <= g_a <= 2^31 -1); (-2^31 <= g_b <= 2^31 -1)
1: x = 2; // h = {#, f_a+3, 3, f_y}; (-2^31 <= g_a <= 2^31 -1); (-2^31 <= g_b <= 2^31 -1); g_x = {#}; g_y = {#}
2: y = 7; // h = {#, f_a+3, 3, f_y}; (-2^31 <= g_a <= 2^31 -1); (-2^31 <= g_b <= 2^31 -1); g_x = {2}; g_y = {#}
3: h = 5; // h = {#, f_a+3, 3, f_y}; (-2^31 <= g_a <= 2^31 -1); (-2^31 <= g_b <= 2^31 -1); g_x = {2}; g_y = {7}
4: x = 4; // h = {5, f_a+3, 3, f_y}; (-2^31 <= g_a <= 2^31 -1); (-2^31 <= g_b <= 2^31 -1); g_x = {2}; g_y = {7}
5: h = b; // h = {5, f_a+3, 3, f_y}; (-2^31 <= g_a <= 2^31 -1); (-2^31 <= g_b <= 2^31 -1); g_x = {4}; g_y = {7}
6: if (h < y) // h = {g_b, f_a+3, 3, f_y}; (-2^31 <= g_a <= 2^31 -1); (-2^31 <= g_b <= 2^31 -1); g_x = {4}; g_y = {7}
{
7: y = 0; // h = {g_b, f_a+3, 3, f_y}; (-2^31 <= g_a <= 2^31 -1); (-2^31 <= g_b <= 2^31 -1); g_x = {4}; g_y = {7}; (h < g_y)
}
else
{
8: x = 3; // h = {g_b, f_a+3, 3, f_y}; (-2^31 <= g_a <= 2^31 -1); (-2^31 <= g_b <= 2^31 -1); g_x = {4}; g_y = {7}; (h >= g_y)
}
9: while (x > 4) // h = {g_b, f_a+3, 3, f_y}; (-2^31 <= g_a <= 2^31 -1); (-2^31 <= g_b <= 2^31 -1); ((g_x == 4 && h < 7) || (g_x == 3 && h >= 7)); ((g_y == 7 && h >= 7) || (g_y == 0 && h < 7))
{ // недостижимо, потому что g_x принимает значение 3 или 4, а в условии цикла g_x > 4
10: if (h > 0) // недостижимо
11: break; // недостижимо
12: x = 1; // недостижимо
13: if (x > 5) // недостижимо
{ // недостижимо
14: y = 6; // недостижимо
} // недостижимо
15: h = y; // недостижимо
} // недостижимо
16:} // Заключительное состояние
// h = {g_b, f_a+3, 3, f_y}; (-2^31 <= g_a <= 2^31 -1); (-2^31 <= g_b <= 2^31 -1); ((g_x == 4 && h < 7) || (g_x == 3 && h >= 7)); ((g_y == 7 && h >= 7) || (g_y == 0 && h < 7))
/////////////////////////
Теперь, после того, как некоторые части функций были объявлены, как недостижимые, это могло повлиять на комбинации условий, что может привести к дальнейшему уменьшению количества состояний, поэтому пересмотрим функции ещё раз, но уже без недостижимых состояний (и сменим нумерацию на новую)
// исходя из функции g - h на входе может быть равна {#} или {5, g_b}, причём т.к. функции выполняются параллельно и мы не знаем времени присваивания h в фукнции g, то придётся всё время считать, что h может быть изменено на {5, g_b}
int h;
