2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки




Начать новую тему Ответить на тему На страницу Пред.  1, 2, 3  След.
 
 Re: Доказательство алгоритма вычисление многочлена
Сообщение04.03.2015, 15:38 
Заслуженный участник


16/02/13
4105
Владивосток
Опять же — доказательство метода, алгоритма и т.п., но не доказательное построение программы.

 Профиль  
                  
 
 Re: Доказательство алгоритма вычисление многочлена
Сообщение04.03.2015, 16:03 


04/06/13
82
Цитата:
Ну вот возьмите хоть мою программу, нарисуйте блок-схему (я б нарисовал, но с рисованием у меня не очень) и попробуйте на ней — только подробно, на каждой стрелке.

Вроде бы так:
Изображение
Прошу прощения, что пределы суммы написаны криво.

-- 04.03.2015, 17:21 --

iifat в сообщении #985541 писал(а):
Опять же — доказательство метода, алгоритма и т.п., но не доказательное построение программы.

Уточню. Если бы функция у нас считала сразу бы по формуле $p=\sum\limits_{i=0}^{n}a_ix^i$.

Вот для этой программы доказательство в моём сообщении всё же не верно или верно?
Используется синтаксис C
// size(a) == n + 1
double horner(double a[], double x, int n)
{
    double p;
    p = 0;
    for (int i = 0; i < n; i++)
        p += a[i] * pow(x, i);
    return p;
}
 

 Профиль  
                  
 
 Re: Доказательство алгоритма вычисление многочлена
Сообщение04.03.2015, 16:28 
Заслуженный участник


16/02/13
4105
Владивосток
Намёк первый: 3) $x=0\wedge i=1$ Вам нужно делать как можно более точные условия, иначе на выходе у вас как раз ваше 7) $i=10$ — абсолютно верно и столь же бесполезно.
Намёк второй: 6) $x=\sum_{k=1}^{i-1}\wedge {i}< {10}$ (мы увеличили $i$ на 1, значит, во входящей формуле надо заменить $i$ на $i-1$). Более того, вот эту самую интересную для нас часть $x=\sum_{k=1}^{i-1}$ надо распространить как можно шире. Попробуйте.

-- 05.03.2015, 00:34 --

Уточню. В оператор $x+=i$ у вас входит стрелка с условием 4)$i<10$, а выходит с условием 5), которое никак из входящего не следует.

-- 05.03.2015, 00:35 --

Gts в сообщении #985552 писал(а):
Вот для этой программы доказательство в моём сообщении всё же не верно или верно?
Нет. Вы исправили метод и доказательство ему, по-моему, теперь соответствует; а вот доказательное программирование — это как на вашей блок-схеме (только правильно :wink: )

 Профиль  
                  
 
 Re: Доказательство алгоритма вычисление многочлена
Сообщение04.03.2015, 17:26 


04/06/13
82
Приведу Ваш участок кода ещё раз:
Используется синтаксис C
int x = 0;
for (int i = 1; i < 10; i++)
    x+=i;
 

Просто мне не понятно: у Вас в
Цитата:
$x=\sum_{k=1}^{i-1}\wedge {i}< {10}$

нижний предел суммы равен $1$ или всё же $0$?

Цитата:
надо распространить как можно шире
Не понял этих слов, но вот что я нарисовал в силу своего разумения.

Изображение

 Профиль  
                  
 
 Re: Доказательство алгоритма вычисление многочлена
Сообщение07.03.2015, 23:08 
Заслуженный участник


16/02/13
4105
Владивосток
Gts в сообщении #985585 писал(а):
нижний предел суммы равен $1$ или всё же $0$?
Ну, в данном случае суммы совпадают, так что не очень важно. С другой стороны, суммирование мы начинаем таки с единицы, так что, на мой взгляд, с единицы правильнее.
4) Нет и нет. В блок проверки условия входят две стрелки, так что условие должно быть записано каким-нибудь общим образом.
6) Что такое $i=\sum_{k=0}^{i+1}k$? И куда делось $1\leq i<10$?
А так всё верно. Можно исправить и переходить к вашей исходной программе.

-- 08.03.2015, 07:13 --

А, впрочем, после инкремента уже не $i<10$, а $i<11$.

 Профиль  
                  
 
 Re: Доказательство алгоритма вычисление многочлена
Сообщение08.03.2015, 00:06 


04/06/13
82
Цитата:
Нет и нет. В блок проверки условия входят две стрелки, так что условие должно быть записано каким-нибудь общим образом.

Хм... тогда пятое условие тоже нужно исправлять.
А вот так будет верно?
4) $i < 10 \wedge i \geqslant 1 \wedge i = \sum\limits_{k=1}^{i}1 \wedge x=\sum\limits_{k=0}^{i - 1}k$

5) $i < 10 \wedge i \geqslant 1 \wedge i = \sum\limits_{k=1}^{i}1 \wedge x=\sum\limits_{k=0}^{i}k$

Цитата:
6) Что такое $i=\sum_{k=0}^{i+1}k$? И куда делось $1\leq i<10$?

Это у меня инкремент так записан. И только сейчас я понял ошибку. Нужно вот так:
6) $i < 11 \wedge i \geqslant 1 \wedge i = \sum\limits_{k=1}^{i+1}1 \wedge x=\sum\limits_{k=0}^{i-1}k$

 Профиль  
                  
 
 Re: Доказательство алгоритма вычисление многочлена
Сообщение08.03.2015, 04:35 
Заслуженный участник


16/02/13
4105
Владивосток
Gts в сообщении #987187 писал(а):
6) $i = \sum\limits_{k=1}^{i+1}1$
Это лишнее вообще, не говоря уж о том, что ересь. Уберите отовсюду.
И правильнее, наверное, будет в 6) $i\geq2$ после инкремента. А вот в 4) всё верно, поскольку две входящих стрелки с условиями 3) и 6).
Ну, можно ещё в 7) подставить 10 вместо $i$ в сумме.

-- 08.03.2015, 12:36 --

Ну, насколько я разбираюсь в предмете, мою простенькую мы сделали. Попробуйте аналогично с вашей.

 Профиль  
                  
 
 Re: Доказательство алгоритма вычисление многочлена
Сообщение08.03.2015, 23:30 


04/06/13
82
Цитата:
Ну, насколько я разбираюсь в предмете, мою простенькую мы сделали. Попробуйте аналогично с вашей.
Не, не. Ещё есть вопросы по Вашей задаче.

Цитата:
Это лишнее вообще, не говоря уж о том, что ересь. Уберите отовсюду.
А как же я тогда в условии скажу, что $i$ инкрементируется? Если я уберу сумму единиц, то в моих условиях больше нечему сказать об инкременте...

 Профиль  
                  
 
 Re: Доказательство алгоритма вычисление многочлена
Сообщение09.03.2015, 03:17 
Заслуженный участник


16/02/13
4105
Владивосток
Gts в сообщении #987598 писал(а):
как же я тогда в условии скажу, что $i$ инкрементируется?
Меняя условие. Во входящем меняем $i$ на $i-1$ и клеим на исходящую стрелку.

 Профиль  
                  
 
 Re: Доказательство алгоритма вычисление многочлена
Сообщение09.03.2015, 18:04 


04/06/13
82
iifat в сообщении #987665 писал(а):
Gts в сообщении #987598 писал(а):
как же я тогда в условии скажу, что $i$ инкрементируется?
Меняя условие. Во входящем меняем $i$ на $i-1$ и клеим на исходящую стрелку.

Ну, у меня вроде такое есть, если выкинуть сумму единиц и учесть Ваше замечание, что после инкремента у нас будет $i \geqslant 2$.

Входящее условие инкремента:
5) $i < 10 \wedge i \geqslant 1 \wedge x=\sum\limits_{k=0}^{i}k$

Исходящее условие инкремента:
6) $i < 11 \wedge i \geqslant 2 \wedge x=\sum\limits_{k=0}^{i-1}k$

Если всё верно, то смотря только на входящее и исходящее условия мне так сразу и не понять, что за оператор у нас между этими условиями. Понять, что сумма $x$ осталась неизменна, а вот $i$ увеличилось, я могу увидеть, если буду видеть и оператор и условия. А ведь по другим то условиям можно понять, что делает оператор, если видеть только условие.

 Профиль  
                  
 
 Re: Доказательство алгоритма вычисление многочлена
Сообщение10.03.2015, 02:19 
Заслуженный участник


16/02/13
4105
Владивосток
Ну, во-первых, понять таки можно, хоть и непросто. Программёж — занятие творческое (лично я в этом убеждён), и в нём таки встречаются непростые задачи.
Gts в сообщении #987846 писал(а):
по другим то условиям можно понять
Не скажите. Просто задачку мы рассматриваем даже не учебную. К примеру, безобиднейший $x=0$ ведёт не просто, как в нашем случае, к приписыванию $\wedge x=0$ — если $x$ у нас участвовал в вычислениях, надо просмотреть входящее условие и исключить его оттуда. В общем, всё решаемо, но не механически.
Во-вторых, задача построения программы по пред- и постусловиям, насколько знаю, не стоит. Либо (правильный способ) пишем программу и одновременно все эти условия, либо по программе пишем условия.

 Профиль  
                  
 
 Re: Доказательство алгоритма вычисление многочлена
Сообщение10.03.2015, 13:07 


04/06/13
82
iifat в сообщении #985158 писал(а):
Вот ещё пример:
Используется синтаксис C
int x = 0; for (int i = 1; i<10; i++) x+=i;
Условие после первого оператора, присваивания, $x=0$; условие в конце тела цикла $1\leq i \wedge i\le10 \wedge x=\sum_{k=1}^ik$

А теперь нарисовав все условия для этой программы, я хочу выбрать для неё инвариант цикла.
В Википедии сказано:
Википедия Инвариант цикла писал(а):
Инвариант строится таким образом, чтобы быть истинным непосредственно перед началом выполнения цикла (перед входом в первую итерацию) и после каждой его итерации.


Перед первой итерацией у нас вот такое условие:
$i < 10 \wedge i \geqslant 1 \wedge x=\sum\limits_{k=0}^{i - 1}k$

После каждой итерации у нас выполняется вот такое условие:
$i \leqslant 10 \wedge i > 1 \wedge x=\sum\limits_{k=0}^{i - 1}k$

Объединив эти условия, получу:
$i \leqslant 10 \wedge i \geqslant 1 \wedge x=\sum\limits_{k=0}^{i - 1}k$
Но уже перед первой итерацией это новое условие не выполнится, так как сумму мы будем считать от $0$ до $-1$, а наш массив вообще не определён на отрицательном интервале, хотя тут сумма должна быть равна $0$.

Прошу помочь с построением инварианта.

-- 10.03.2015, 14:45 --

Приложу и блок-схему
Изображение

 Профиль  
                  
 
 Re: Доказательство алгоритма вычисление многочлена
Сообщение10.03.2015, 15:50 
Заслуженный участник


16/02/13
4105
Владивосток
Ну, непосредственно перед началом цикла у нас условие 3, после итерации — 6. Поменять в 6-м $\gt1$ на $\geq1$ — получим общее условие. 3 и 6 можно поменять на него. Оно и будет инвариантом цикла.

 Профиль  
                  
 
 Re: Доказательство алгоритма вычисление многочлена
Сообщение10.03.2015, 16:05 


04/06/13
82
iifat в сообщении #988219 писал(а):
Ну, непосредственно перед началом цикла у нас условие 3, после итерации — 6. Поменять в 6-м $\gt1$ на $\geq1$ — получим общее условие. 3 и 6 можно поменять на него. Оно и будет инвариантом цикла.

Вот за эти слова "непосредственно перед началом цикла у нас условие 3" отдельное спасибо. Упустил я этот момент.


Цитата:
Но уже перед первой итерацией это новое условие не выполнится, так как сумму мы будем считать от $0$ до $-1$, а наш массив вообще не определён на отрицательном интервале, хотя тут сумма должна быть равна $0$.
Как же это я такое написал... Почему то решил, что в начале $i$ будет равно 0, а не 1.

 Профиль  
                  
 
 Re: Доказательство алгоритма вычисление многочлена
Сообщение11.03.2015, 13:23 
Заслуженный участник


16/02/13
4105
Владивосток
Gts в сообщении #988223 писал(а):
Как же это я такое написал
Что именно? Сумма от нуля до минус единицы — совершенно добропорядочная сумма по пустому множеству индексов. Она равна нулю.

 Профиль  
                  
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 42 ]  На страницу Пред.  1, 2, 3  След.

Модераторы: Karan, Toucan, PAV, maxal, Супермодераторы



Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group