Смекни!
smekni.com

Спецификация программы uWert > Текст программы uWert Доказательство корректности программы uWert Организация многооконного интерфейса и диалога в приложениях (стр. 5 из 10)

Тогда cтек имеет rk+1 ячеек. Переменная lb будет равна lbDig. Ячейка rk содержит число n+F(Y)+F(Z\M(Y\m)) = n+F(Y+Z\M(Y\m) в обозначениях случая А. Ячейка rk+1 содержит число F(M(Z\m)) = F(M(Y+Z\m)). То есть, при обработке Y+Z реализован случай B.

Пусть при обработке Z реализован случай С.

Тогда cтек имеет rk+1 ячеек. Переменная lb будет равна lbRBr. Ячейка rk содержит число n+F(Y)+F(Z\M(Y)) = n+F(Y+Z\M(Y) в обозначениях случая А. Ячейка rk+1 содержит число F(M(Z)) = F(M(Y+Z)). То есть, при обработке Y+Z реализован случай С.

2.3. Пусть X=Y*Z. Рассмотрим представление (разложение) X = Y*Z\M(Y*Z)+M(Y*Z).

Если обе части разложения не пусты, то применим к ним предположение индукции п.2.2 теоремы.

Рассмотрим случай, когда M(Y*Z) пусто. Тогда существуют такое РАВ Q и число m, что Y*Z =Q+m. Применим к ним предположение индукции п.2.2 теоремы.

Рассмотрим случай, когда Y*Z\M(Y*Z) пусто, то есть, Y*Z – мультипликативный РАВ.

Тогда применим Программу к Y, как в п.2.2. Тогда после обработки Y* Программа придёт в следующее состояние. Переменная lb = lbSign, стек содержит rk+1 ячеек, в ячейке rk содержится исходное число n. Ячейка rk+1 содержит число F(X), а знак является знаком операции умножения.

Рассмотрим применение в этих условиях Программы к Z индукцией по построению Z.

I. База индукции.

1.1. Пусть Z является нумералом m. Тогда на выходе из его обработки переменные fdig и ldig указывают начало и, соответственно, конец этого нумерала. Стек содержит те же rk+1 ячеек. Число в ячейке rk+1 F(X) = F(Y) = F(Y*m\m) = F(X\m). То есть, выполняются условия случая B.

1.2. Пусть Z является (Y). Тогда нетрудно убедиться, как в п.2.1 выше, после обработки Программой такого Z установятся условия случая C. Число в ячейке rk+1 F(X) = F(Y)*F(Z)=D(Y*Z).

II. Шаг индукции. Пусть X=Y*Z*m.

2.1. Пусть X=Y*Z*m. По предположению индукции после обработки Y*Z установятся условия теоремы. Применяя рассуждения п.1.1, можно убедиться, что после обработки m установятся условия случая B. Число в ячейке rk+1 F(X\m) = F(Y*Z*m\m) = F(Y)*F(Z*m\m).

2.2. Пусть X=Y*Z*(U). По предположению индукции после обработки Y*Z установятся условия теоремы. Применяя рассуждения п.1.2, можно убедиться, что после обработки (U) установятся условия случая C. Число в ячейке rk+1 F(X) = F(Y*Z*(U)) = F(Y)*F(Z)*F(U)) = F(Y)*F(Z*(U)).

Теорема доказана.

Следствие. Если программу uWert применить к РАВ X, то в качестве результата будет получено число F(X).

Доказательство. Пусть Программа применяется к РАВ X. Нетрудно убедиться, что при входе в цикл выполняются условия Теоремы 1, причём стек содержит одну ячейку, то есть, k=1, n=0 и z=’+’. Поэтому Программа выйдет из цикла и перейдёт к процедуре spin(i, ‘F’) , установив один из 3 случаев состояния, указанных в Теореме.

Рассмотрим действия процедуры spin(i, ‘F’) в каждом из этих случаев.

Случай А.

В строке 18 число в ячейке 1 складывается с числом в конце X. В результате это число становится равным F(X).

Случай B.

Стек содержит 2 ячейки. Строка 13 умножает число из ячейке 2 на число в конце X. Затем в строках 15 и 16 произведение складывается с числом в ячейке 1, а ячейка 2 выводится из стека. В результате единственная ячейка стека содержит F(X).

Случай C. Стек содержит 2 ячейки. Строка 14 временно сохраняет число из ячейки 2. Затем в строках 15 и 16 оно складывается с числом в ячейке 1, а ячейка 2 выводится из стека. В результате единственная ячейка стека содержит F(X).

Число из ячейки стека выводится в окно eValue.

Что и требовалось доказать.

УПРАЖНЕНИЯ

1. Оцените конструктивную сложность программы по M.Холстеду.

2. Оцените вычислительную сложность программы.


5. ОРГАНИЗАЦИЯ МНОГООКОННОГО ИНТЕРФЕЙСА И ДИАЛОГА В ПРИЛОЖЕНИЯХ

5.1. Многооконный интерфейс на основе сохраняемых форм

5.2. Диалог на основе динамически создаваемых форм

5.2.1. Проект диалоговой функции в Delphi

unit CyrDialog;

interface

////////////////////////////////////////////////////////////////////////////////

//* Модуль обеспечивает диалог приложения с пользователем

//* и для этой цели предоставляет функцию Rudial, аналогичную

//* функции MessageDLG. Отличие состоит в том, что Rudial

//* показывает кнопки с русскязычными надписями.

uses classes, forms, dialogs, stdctrls, controls;

type TDForm = class(TCustomForm)end;

function Rudial(const Msg: string; DlgType: TMsgDlgType; Buttons: TMsgDlgButtons; HelpCtx: Longint): Word;

var vform: TDForm;

implementation

uses math, graphics, windows, sysutils;

function Rudial(const Msg: string; DlgType: TMsgDlgType; Buttons: TMsgDlgButtons; HelpCtx: Longint): Word;

var vbut: TButton; vt: TLabel; i, n: integer;

ab: array [1..11]of string; mr: array [1..11]of TModalResult;

begin

n:=0;

if mbOK in Buttons then begin inc(n); ab[n]:='О''КЭЙ'; mr[n]:=mrOK end;

if mbYes in Buttons then begin inc(n); ab[n]:='ДА'; mr[n]:=mrYES end;

if mbNO in Buttons then begin inc(n); ab[n]:='НЕТ'; mr[n]:=mrNO end;

if mbCancel in Buttons then begin inc(n); ab[n]:='ОТМЕНА'; mr[n]:=mrCancel end;

if mbAbort in Buttons then begin inc(n); ab[n]:='БАСТА'; mr[n]:=mrAbort end;

if mbRetry in Buttons then begin inc(n); ab[n]:='ПОВТОР'; mr[n]:=mrRetry end;

if mbIgnore in Buttons then begin inc(n); ab[n]:='НУ И ЧТО'; mr[n]:=mrIgnore end;

if mbAll in Buttons then begin inc(n); ab[n]:='ВСЕ'; mr[n]:=mrALL end;

if mbNoTOALL in Buttons then begin inc(n); ab[n]:='НИКАКИЕ'; mr[n]:=mrALL+1 end;

if mbYEStoALL in Buttons then begin inc(n); ab[n]:='ВСЕ'; mr[n]:=mrYEStoALL end;

try

vform:=TDForm.CreateNew(Application);

with vform do

begin

Height:=110;

BorderStyle:=bsDialog;

caption:='Ответьте нажатием кнопки.';

position:=poScreenCenter;

BorderWidth:=3;

FormStyle:=fsStayOnTop;

vt:=TLabel.Create(vform);

vt.parent:=vform;

vt.AutoSize:=true;

vt.caption:=msg;

vt.Font.Style:=[fsBold];

Width:=max(vt.width+50,70*n+24*(n-1)+50);

vt.top:=10;

vt.left:=(width-vt.width)div 2;

for i:=1to n do

begin

vbut:=TButton.Create(vform);

with vbut do

begin

parent:=vform;

top:=40;

width:=70;

height:=23;

left:=(vform.width-70*n-20*(n-1))div 2+(i-1)*(70+20);

Caption:=ab[i];

font.style:=[fsBold];

ModalResult:=mr[i]

// onClick:=CliRu

end

end;

result:=ShowModal;

FreeAndNil(vform)

end

finally

if not(vform=nil)then vform.free

end

end;

{procedure TDForm.CliRu(sender: TObject);

begin

TForm(TComponent(sender).owner).close

end;}

end.

5.2.2. Проект диалоговой функции в Microsoft Visual Studio 2008 (CLR, язык C#)

В среде проектирования включение дополнительных форм в проект обеспечивается в главном меню командами Проект – Добавить форму Windows …. В результате открывается окно выбора элемента, в котором уже выбран пункт “Форма Windows Form”. Пользователю достаточно нажать экранную кнопку Добавить. В это же окно можно попасть, активируя другие подпункты пункта главного меню Проект, начинающиеся со cлова Добавить.

В проект будет добавлены файлы с именем новой формы и расширением cs и Designer.cs. К новой форме можно обращаться при запуске приложения, выполнив предложения:

System.Windows.Forms.Form vbox;//объявление переменной

vbox = new NBox();//создание экземпляра формы.

Далее её можно сделать, например, сделать видимой на равне с главной формой предложением:

vbox.Show ();

или видимой в модальном режиме, то есть в режиме вызова (с приостановкой активности вызывающей формы:

vbox.ShowDialog();

Кроме того форму можно определить и использовать без “дизайнера”, то есть отдельного модуля, обеспечивающего хранение содержимого формы и заполнение её при запуске. Для этого достаточно определить соответствующий класс и вызывать его конструктор, а заполнение формы обеспечивать по месту этого вызова.Такой случай показан в нижеследующем приложении.

Главная форма:

using System;

using System.Collections.Generic;

using System.ComponentModel;

using System.Data;

using System.Drawing;

using System.Linq;

using System.Text;

using System.Windows.Forms;

namespace WinForm12

{

public partial class Form1 : Form

{

public Form1()

{

InitializeComponent();

}

private void button1_Click(object sender, EventArgs e)

{

NBox.PseudoFun();

// this.Close();

}

}

}

Наряду с главной формой Form1 в проекте имеется модуль NewBox.cs:

using System;

using System.Windows.Forms;

//using NUnit.Framework;

namespace WinForm12

{

public class NBox : Form

{

public static void PseudoFun()

{

// MessageBox.Show("bingo!");

System.Windows.Forms.Form vbox;

vbox = new NBox();

vbox.Name = "NBox";

System.Windows.Forms.Button vbut;

vbut = new System.Windows.Forms.Button();

// vbut.Show();

vbut.Location = new System.Drawing.Point(100, 100);

vbut.Size = new System.Drawing.Size(100,30);

vbut.Text = "ЖМИ";

vbox.Controls.Add(vbut);

// vbut.Click += new EventHandler(NBox.vbut_Click);

vbut.Click += NBox.vbut_Click;

vbox.ShowDialog();

}

public void Main()

{

MessageBox.Show("bingo!");

}

public NBox()

{

InitializeForm();

}

private void InitializeForm()

{

this.Text = "Nbox";

}

private static void vbut_Click(object sender, EventArgs e)

{

// System.Windows.Forms.Button lbut;

// lbut = sender as Button;

// System.Windows.Forms.Form lbox;

// lbox = lbut.Parent as Form;

// MessageBox.Show(lbox.Text);

// lbox.Close();

((sender as Button).Parent as Form).Close();

}

}

}

В этом модуле содержится класс NBox, определяющий форму и включающий в себя статический метод PseudoFun, который создаёт экземпляр формы NBox, заносит на неё кнопку и обработчик её нажатия и вызывает форму в модальном режиме.

using System;

using System.Windows.Forms;

namespace WinForm12

{

public class NBox : Form

{

public static void PseudoFun()

{

System.Windows.Forms.Form vbox;

vbox = new NBox();

vbox.Name = "NBox";

System.Windows.Forms.Button vbut;

vbut = new System.Windows.Forms.Button();

vbut.Location = new System.Drawing.Point(100, 100);

vbut.Size = new System.Drawing.Size(100,30);

vbut.Text = "ЖМИ";

vbox.Controls.Add(vbut);

// vbut.Click += new EventHandler(NBox.vbut_Click);

vbut.Click += NBox.vbut_Click;

vbox.ShowDialog();

}

public NBox()

{

InitializeForm();

}

private void InitializeForm()

{

this.Text = "Nbox";

}

private static void vbut_Click(object sender, EventArgs e)

{

// System.Windows.Forms.Button lbut;

// lbut = sender as Button;

// System.Windows.Forms.Form lbox;

// lbox = lbut.Parent as Form;

// lbox.Close();

((sender as Button).Parent as Form).Close();

}

}

}

5.2.3. Проект диалоговой функции в Microsoft Visual Studio 2008 (CLR, язык C++)

Приложение, аналогичное последнему, рассмотренному в предыдущем разделе, можно построить в той же среде проектирования, но для языка C++.

В этом случае проект содержит главный файл с расширением cpp, а именно:

CLRWin02.cpp: главный файл проекта.

#include "stdafx.h"

#include "TestForm.h"

using namespace CLRWin02;

int nn=25;

[STAThreadAttribute]

int main(array<System::String ^> ^args)

{

// Включение визуальных эффектов Windows XP до создания каких-либо элементов управления

Application::EnableVisualStyles();

Application::SetCompatibleTextRenderingDefault(false);

// Создание главного окна и его запуск

Application::Run(gcnew TestForm());

return 0;

}

Модуль NewBox.h, содержащий определение формы, которая динамически создавается и вызывается в модальном режиме из модуля TestForm.h.

#pragma once

#include "NewBox.h"

namespace CLRWin02 {

using namespace System;

using namespace System::ComponentModel;

using namespace System::Collections;

using namespace System::Windows::Forms;

using namespace System::Data;

using namespace System::Drawing;