Аннотирование процедур

Аннотирование процедур

{Pre:P}

{Post:Q}

Proc <идентификатор> (<спецификация параметров>)

Этого достаточно, тело не рассматриваем Þ использовать глобальные переменные нельзя.

В Р могут входить параметры с атрибутами

                        value

            value result

B Q:                value result

Рекомендуемые материалы

                        result

Рассмотрим процедуру поиска элемента массива

{Pre: n=N Ù x=X Ù XÎB[0:N-1] Ù b=B}

{Post: 0£i<N Ù B[i]=X}

Proc search (  value n,x:integer;

value b; array of integer;

result i: integer );

Тело:

            {i:=0}

     {инвариант: 0£i<N Ù XÎB[i:N-1]}

     {ограничение  N-i}

     do b[i]¹x ® i:=i+1 od

Вариант, который будем рассматривать дальше

Описание вызова:

P()          x,y,z – формальные параметры – параметры

                             а,b,c  - фактические параметры – аргументы

a_i – входные аргументы

b_i – входные/выходные аргументы

с_i – выходные аргументы

Вызов нашей процедуры:

Вам также может быть полезна лекция "2.2. Двоичная система счисления".

search(50,t,c,position[i])

Алгоритм вызова процедуры

1. определяются значения аргументов  и  и записываются в параметре и , причем в  может быть выражение.

2. определяются переменные, описываемые и .

3. выполняется тело процедуры

4. значение выходных параметров и  записываются в выходные аргументы и .