Доказательство алгоритма вычисление многочлена

[iifat]

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

[Gts]

Цитата:

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

Вроде бы так:

Прошу прощения, что пределы суммы написаны криво.

-- 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;
}
 

[iifat]

Намёк первый: 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 писал(а):

Вот для этой программы доказательство в моём сообщении всё же не верно или верно?

Нет. Вы исправили метод и доказательство ему, по-моему, теперь соответствует; а вот доказательное программирование — это как на вашей блок-схеме (только правильно )

[Gts]

Приведу Ваш участок кода ещё раз:

Используется синтаксис C

int x = 0;
for (int i = 1; i < 10; i++)
    x+=i;
 

Просто мне не понятно: у Вас в

Цитата:

$x=\sum_{k=1}^{i-1}\wedge {i}< {10}$

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

Цитата:

надо распространить как можно шире

Не понял этих слов, но вот что я нарисовал в силу своего разумения.

[iifat]

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$.

[Gts]

Цитата:

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

Хм... тогда пятое условие тоже нужно исправлять.
А вот так будет верно?
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$

[iifat]

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 --

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

[Gts]

Цитата:

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

Не, не. Ещё есть вопросы по Вашей задаче.

Цитата:

Это лишнее вообще, не говоря уж о том, что ересь. Уберите отовсюду.

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

[iifat]

Gts в сообщении #987598 писал(а):

как же я тогда в условии скажу, что $i$ инкрементируется?

Меняя условие. Во входящем меняем $i$ на $i-1$ и клеим на исходящую стрелку.

[Gts]

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$ увеличилось, я могу увидеть, если буду видеть и оператор и условия. А ведь по другим то условиям можно понять, что делает оператор, если видеть только условие.

[iifat]

Ну, во-первых, понять таки можно, хоть и непросто. Программёж — занятие творческое (лично я в этом убеждён), и в нём таки встречаются непростые задачи.

Gts в сообщении #987846 писал(а):

по другим то условиям можно понять

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

[Gts]

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 --

Приложу и блок-схему

[iifat]

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

[Gts]

iifat в сообщении #988219 писал(а):

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

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

Цитата:

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

Как же это я такое написал... Почему то решил, что в начале $i$ будет равно 0, а не 1.

[iifat]

Gts в сообщении #988223 писал(а):

Как же это я такое написал

Что именно? Сумма от нуля до минус единицы — совершенно добропорядочная сумма по пустому множеству индексов. Она равна нулю.