end;
function Stack.show(n:integer):R;
begin
result:=ar[n]
end;
procedure TForm1.Button1Click(Sender: TObject);
var i, n, fdig, ldig: integer; result: integer;wr: R;
function SelectDigit: integer;
begin //involve sign of the number
if(fdig>2)and((eExpression.text[fdig-1]='-')or(eExpression.text[fdig-1]='+'))
and((eExpression.text[fdig-2]='-')or(eExpression.text[fdig-2]='+')
or(eExpression.text[fdig-2]='*')or(eExpression.text[fdig-2]='/')
or(eExpression.text[fdig-2]='('))
or(fdig=2)and ((eExpression.text[1]='-')or(eExpression.text[1]='+'))
then fdig:=fdig-1;
result:=StrToInt(copy(eExpression.text, fdig, ldig-fdig+1))
end;
function Calc(n,m: integer; s: char): integer;
begin
if s='+'then result:=n+m
else result:=n-m
end;
procedure Alloc(v: integer;s: char);//sign upon digit
var vp: integer; sp: char;
begin
1: wr:=buf.pop;
2: if wr.sgn='*'
3: then if s='*'//sgn='*'
4: then wr.va:=wr.va*v
5: else begin //s='+' or '-'
6: vp:=wr.va*v;
7: wr:=buf.pop;//delete multiplicative cell
8: wr.va:=Calc(wr.va,vp,wr.sgn)//update last cell
9: end
10: else if s='*'//sgn='+' or '-'
11: then begin
12: buf.push(wr);//additive part is restored
13: wr.va:=v
14: end
15: else wr.va:=Calc(wr.va,v,wr.sgn);
16: wr.sgn:=s;
17: buf.push(wr)
end;
procedure Sab(c: char);//sign upon bracket
var vp: integer;
begin
1: wr:=buf.pop;
2: if wr.sgn='*'
3: then if not(c='*')//'+' or '-'
4: then begin
5: vp:=wr.va;
6: wr:=buf.pop;//delete bracket cell
7: wr.va:=Calc(wr.va,vp,wr.sgn)//update last cell
8: end;
9: wr.sgn:=c;
10: buf.push(wr)
end;
procedure spin(i: integer; c: char);
var vp: integer;
begin
1: case c of
2: '(': if(lb=lbNone)or(lb=lbSign)or(lb=lbLBr)
3: then begin
4: with wr do begin va:=0; sgn:= '+'end;
5: buf.push(wr);//create new additive cell
6: lb:=lbLBr;
7: end
8: else raise Exception.Create('Wrong sequence!');
9: ')','F': begin
10: wr:=buf.pop;
11: if wr.sgn='*'
12: then begin //sgn='+' or '-'
13: if lb=lbDig then vp:=wr.va*SelectDigit
14: else vp:=wr.va;
15: wr:=buf.pop;
16: wr.va:=Calc(wr.va,vp,wr.sgn)
17: end
18: else if lb=lbDig then wr.va:=Calc(wr.va,SelectDigit,wr.sgn);
19: if c=')'then begin
20: vp:=wr.va;
21: wr:=buf.pop;
22: if wr.sgn='*'then wr.va:=wr.va*vp
23: else begin
24: buf.push(wr);//restore cell to create
25: wr.va:=vp;//cell for case of future
26: wr.sgn:='*'//multiplication
27: end;
28: lb:=lbRBr
29: end;
30: buf.push(wr)
31: end;
32: '+','-','*':
32: begin
33: if((c='*')or(c='/'))and((lb=lbNone)or(lb=lbLBr))then raise Exception.Create('wrong input digit');
34: if lb=lbDig then Alloc(SelectDigit,c);
35: if lb=lbRBr then Sab(c);
36: lb:=lbSign
37: end;
38: '0','1','2','3','4','5','6','7','8','9':
39: begin
40: if(lb=lbNone)or(lb=lbSign)or(lb=lbLBr)
41: then begin
42: fdig:=i;
43: ldig:=i;
44: lb:=lbDig
45: end
46: else ldig:=i;
47: if lb=lbRBr then raise Exception.Create('Wrong sign sequence'+ ' '+IntToStr(i));
48: end
49: end//case
end;
begin
buf:=Stack.create(self);
with wr do begin va:=0; sgn:= '+'end;
buf.push(wr);
lb:=lbNone;
try
for i:=1to length(eExpression.text)do spin(i, eExpression.text[i]);
if(lb=lbDig)or(lb=lbRBr)
then
else raise Exception.Create('wrong end of input'+ ' '+IntToStr(i));
spin(i,'F');
eValue.text:=IntToStr(buf.pop.va);
if buf.Depth>1then raise Exception.Create('wrong end of input!')
except
on E: Exception do begin showmessage(E.message);buf.Destroy end
end
end;
end.
4.3. Доказательство корректности программы uWert
Концепция программы состоит в следующем:
1) исходное РАВ обрабатывается в цикле литера за литерой по одной литере на каждом шаге цикла, без возвратов,
2) рабочая информация накапливается в стеке и переменных fdig, ldig и lb,
3) ячейка стека содержит промежуточный результат вычисления или его часть,
4) переменные fdig и ldig – это номера первой и последней литеры “текущего” нумерала, то есть нумерала, в пределах которого находится переменная цикла,
5) переменная lb хранит литеру, предшествующую “текущей”, то есть литере, номер которой в исходном РАВ совпадает со значением переменной цикла.
Для более формального исследования программы и доказательства её корректности далее приведён ряд определений.
“Мультипликативное окончание” М(X) для РАВ X определяется индукцией по построению X:
I. База индукции.
1.1. Если X – нумерал, то M(X) = ‘’ (то есть, мультипликативное окончание отсутствует).
1.2. Если X = m*n , где m и n – нумералы, то M(X) = X.
II. Шаг индукции:
2.1. М((X)) = (X), (то есть, РАВ (X) совпадает со своим мультипликативным окончанием).
2.2. M(Y+Z) = M(Z).
2.3. M(Y-Z) = M(Z).
2.4. M(Y*Z) = M(Y)*Z, если M(Z) = Z, иначе M(Y*Z) = M(Z).
Очевидно, что если M(X) не пусто, то М(X) является РАВ.
Мультипликативным называется РАВ, совпадающее со своим окончанием.
Выражение X\Y определено, если только существует такое Z, что X=ZY и тогда X\Y = Z.
Функция F(X) от регулярного арифметического выражения (РАВ) определяется по индукции:
I. База индукции. Если ‘X’ - нумерал, то F(X) = StrToInt(‘X’).
II. Шаг индукции:
2.1. Если X и Y являются РАВ, то
F(X+Y) = F(X)+F(Y),
F(X-Y) = F(X)-F(Y).
2.2. F(X*Y) = F(X)*F(Y), если M(X) = X и M(Y) = Y,
иначе F(X*Y) = F(X*Y\M(Y))+F(M(Y)).
F от пустой строки равно 0.
Теорема 1. Пусть программа uWert (далее просто Программа) применяется к слову eExpression.Text = ‘AXB’, где X – РАВ, а B – строка, которая может быть пустой, и приступает к выполнению процедуры spin в цикле при i = length(‘A’)+1, причём:
a) lb = lbNone, если A пуста, или lb = lbSign или lb = lbLBr, в противном случае,
b) стек buf содержит последовательность ячеек r1, …, rk, и ячейка rk содержит число n и знак операции ‘+’ или ‘-’.
Тогда на шаге i = length(‘AX’) цикла на выходе процедуры spin установится одно из следующих состояний.
Случай А.
lb = lbDig,
переменные fdig и ldig указывают начало и, соответственно, конец нумерала m, завершающего X,
стек buf содержит последовательность ячеек r1, …, rk, и ячейка rk содержит число n + F(X\m) и прежний знак операции ‘+’ или ‘-’.
Случай В.
lb = lbDig,
переменные fdig и ldig указывают начало и, соответственно, конец нумерала m, завершающего X,
стек buf содержит последовательность ячеек r1, …, rk, rk+1, ячейка rk содержит число n + F(X\S) и прежний знак операции, а rk+1 содержит число F(S\m) и знак операции ‘*’, при этом S – мультипликативное окончание X. Если X – мультипликативное РАВ, то F(X\S)=0.
Случай С.
lb = lbRBr,
стек buf содержит последовательность ячеек r1, …, rk, rk+1, ячейка rk содержит число n+ F(X\S) и прежний знак операции, а rk+1 содержит число F(S) и знак операции ‘*’, при этом S – мультипликативное окончание X. Если X – мультипликативное РАВ, то F(X\S)=0.
Доказательство. Проводится индукцией по построению X как РАВ.
I. База индукции. Пусть X - нумерал (то есть последовательность цифр без знака и без пробелов).
Тогда Программа выполнит length(‘X’) шагов цикла, в которых будут работать строки 39 - 48 процедуры spin, переменные fdig и ldig установится на начало и, соответственно, конец строки X, а lb будет устанавливаться равным lbDig на всех шагах до шага length(‘X’) включительно. Стек не изменяется. То есть, реализуется случай А.
II. Шаг индукции.
2.1. Пусть X = (Y), где Y – РАВ.
Тогда в результате выполнения строк 2 – 7 процедуры spin в стек будет добавлена ячейка rk+1, содержащая число 0 и знак ‘+’, и, таким образом, перед следующим выполнение шага цикла для Y установятся условия данной леммы, причём lb = lbLBr, B = ‘)B’. По предположению индукции Программа выполнит length(Y) шагов цикла и на последнем из них на выходе из процедуры spin установится состояние, соответствующее одному из 3 указанных случаев.
Пусть реализован случай А.
Тогда на следующем шаге цикла в результате выполнения строк 18 – 26 к числу в ячейке rk+1 будет прибавлено число m и установлен знак операции ‘*’. Эта ячейка будет содержать F(‘X). В строке 28 переменной lb будет присвоено значение lbRBr, то есть, в данном случае при обработке (X) реализуется случай C.
Пусть реализован случай В.
Тогда на следующем шаге цикла в результате выполнения строк 13, 15 и 16 ячейка rk+2 снимается со стека, число из ячейки rk+2 умножается на число m, со стека снимается ячейка rk+1 и произведение складывается с её содержимым. Затем в строке 21 снимается ячейка rk, но поскольку в ней указана аддитивная операция, в строке 24 она возвращается в стек, в строке 30 в стек вводится ячейка rk+1, а строки 25 и 26 обеспечивают в ней вычисленную в строке 16 сумму и знак умножения.
Таким образом, в данном случае при обработке (X) реализуется случай C.
Пусть реализован случай C.
Тогда на следующем шаге цикла в результате выполнения строки 10 ячейка rk+2 снимается со стека, и число из неё в строке 14 временно сохраняется. Затем в строке 15 со стека снимается ячейка rk+1, и в строке 16 число из ячейки rk+1 складывается с сохранённым числом – результатом обработки X и в строке 20 временно сохраняется. Затем в строке 21 со стека снимается ячейка rk, но поскольку в ней указана аддитивная операция, в строке 24 она возвращается в стек, в строке 30 в стек вводится ячейка rk+1, а строки 25 и 26 обеспечивают в ней сохранённое число и знак умножения.
Таким образом, в данном случае при обработке (X) реализуется случай C.
2.2. Пусть X= YwZ, где Y и Z – РАВ, а w – ‘+’ или ‘-’.
Тогда применим индукционное предположение к Y и рассмотрим случаи.
Пусть реализован случай А.
Тогда на следующем шаге цикла в результате выполнения строки 35 вызывается процедура Alloc. В ней в строке 15 число, выделенное значениями переменных fdig и ldig, складывается с числом в ячейке rk. В результате число в ячейке rk становится равным n+F(X). Строки 1, 16 и 17 обеспечивают занесение его в эту ячейку Переменная lb устанавливается равной lbSign.
Пусть реализован случай B.
Тогда на следующем шаге цикла в результате выполнения строки 35 вызывается процедура Alloc. В ней в строке 6 число, выделенное значениями переменных fdig и ldig, умножается на число в ячейке rk+1, а в строках 7 и 8 складывается с числом из ячейки rk. Строки 1, 16 и 17 обеспечивают занесение суммы в эту ячейку и установку в ней w как знака операции. В результате число в ячейке rk становится равным n+F(X). Переменная lb устанавливается равной lbSign.
Пусть реализован случай С.
Тогда на следующем шаге цикла в результате выполнения строки 36 вызывается процедура Sab. В ней в строке 7 число, сформированное в ячейке rk, складывается с числом или вычитается из числа, сформированного в ячейке rk+1. В результате число в ячейке rk становится равным n+F(X). Переменная lb устанавливается равной lbSign.
Далее Программа применяется к Z и по предположению индукции Программа переходит к одному из случаев, определённых в формулировке леммы.
Пусть при обработке Z реализован случай А.
Пусть при обработке Z реализован случай B.