 |
Листинг 21.1. Программа управления инъекциями инсулина
|
|
|
|
//Вводимая доза инсулина является функцией уровня сахара в крови,
//предыдущей суммарной введенной дозы и времени предыдущей инъекции
currentDose = computelnsulin ();
//Проверка безопасности: если необходимо, изменяется currentDose
//1-й оператор if
if (previousDose == 0)
{
if(currentDose > 16)
currentDose = 16;
}
else
if (currentDose > (previousDose * 2))
currentDose = (previousDose * 2;
//2-й оператор if
if (currentDose < minimumDose)
currentDose = 0;
else if (currentDose > maxDose)
currentDose = maxDose;
administerlnsulin (currentDose);
Доказательство безопасности для данного кода включает доказательство того, что вводимая доза инсулина никогда не превысит максимальный уровень, отдельно установленный для каждого больного диабетом. Таким образом, совсем необязательно доказывать, что система выдает "правильную" дозу, достаточно доказать, что пациенту никогда не будет выдана слишком большая доза инсулина.
Для построения доказательства безопасности находим предусловие для опасного состояния, в данном случае это условие currentDose > maxDose. Затем необходимо показать, что все ветви программы приводят к противоречию с данным условием. Если это действительно так, то условие опасного состояния никогда не будет истинным, а следовательно, система безопасна.
Доказательство безопасности, подобное представленному на рис. 21.6, намного короче, чем формальная верификация системы. Сначала определяются все возможные ветви, которые приводят к потенциально опасному состоянию. Для этого необходимо пройти в обратном порядке все ветви, идущие от данного опасного состояния, и рассмотреть последнее присвоение у всех переменных состояния на каждой ветви. Предыдущие вычисления (например, 1-й оператор if на рис. 21.6) можно не рассматривать. В этом примере нам необходимо рассмотреть набор возможных значений переменной currentDose (текущая доза) непосредственно перед выполнением метода administerlnsulin (регулирование инсулина).
|
|
|
Рис. 21.6. Доказательство безопасности методом от противного
В представленном на рис. 21.6 доказательстве вызов метода administerlnsulin возможен в трех ветвях программы.
1. Ни одно из ответвлений 2-го оператора if не выполняется. Данная ситуация имеет место, если значение переменной CurrentDose больше или равно minimumDose (минимальная доза) и меньше или равно maxDose (максимальная доза).
2. Выполняется ветвь then 2-го оператора if. В этом случае currentppse присваивается значение нуль. Здесь постусловием будет currentDose = 0.
3. Выполняется ветвь else 2-го оператора if. В этом случае currentDose присваивается значение maxDose. Постусловием этой ветви будет currentDose = maxDose.
Во всех трех случаях постусловие противоречит предусловию опасного состояния, поэтому система безопасна.
|
|
|
I. Нижний уровень блоков управления в инкубаториях
II. ПРОГРАММА ТЕОРЕТИКО-ПРИКЛАДНОГО СОЦИОЛОГИЧЕСКОГО ИССЛЕДОВАНИЯ
II. Программа теоретического раздела дисциплины
II. ПРОГРАММА УЧЕБНОЙ ПРАКТИКИ
III.2. Условная структура управления
IV. Циклдік оператор алгоритмдерін программалау
TARP — программа развития чтения при помощи магнитофона
V. ОСНОВНЫЕ ТРЕБОВАНИЯ К РАЗВИТИЮ СТУДЕНЧЕСКОГО САМОУПРАВЛЕНИЯ
V. Программа соревнований
V. Программа соревнований.
