Карта сайта

Это автоматически сохраненная страница от 12.11.2013. Оригинал был здесь: http://2ch.hk/b/res/57288949.html
Сайт a2ch.ru не связан с авторами и содержимым страницы
жалоба / abuse: admin@a2ch.ru

Втр 12 Ноя 2013 02:51:08
S ::= a := 0;
while x 0 do
a := a + 3;
x := x - 1
od;
x := a;
y := y - 1;
while y 0 do
a := a + x;
y := y - 1
od

Доказать в H*: <x = X > 0 y = Y > 0>S<a = 3XY>


Втр 12 Ноя 2013 03:00:57
>>57288949
1 = 1/3 * 3 = 0.(3) * 3 = 0.(9)

Втр 12 Ноя 2013 03:04:12
>>57288949
Но это же очевидно, ОП, не верю, что ты это не понимаешь, и несмотря на это запостил в таком непонятном виде.

>>57289153
И чо?

Втр 12 Ноя 2013 03:04:59
>>57289206
Соси.

Втр 12 Ноя 2013 03:06:10
>>57289227
Или что?

Втр 12 Ноя 2013 03:08:27
>>57289206
>Но это же очевидно, ОП,
Сформулируй инварианты и скажи во сколько высказываний уместилось доказательство.

Втр 12 Ноя 2013 03:09:40
>>57289243
Или давай в очко.

Втр 12 Ноя 2013 03:11:11
>>57289279
> Доказать в H*
Ах вот же что.
Объяви раздел науки, определи H* или зачем ты вообще это писал?
Ну и поясни первую строку, конечно :3

Втр 12 Ноя 2013 03:12:09
>>57289303
А если не буду?

Втр 12 Ноя 2013 03:12:09
>>57289334
Твоя мамаша.

Втр 12 Ноя 2013 03:12:40
>>57289345
Ну и похуй тогда.

Втр 12 Ноя 2013 03:13:08
>>57289346
Попизди мне тут.

Втр 12 Ноя 2013 03:14:25
>>57289358
Пизжу тут.

Втр 12 Ноя 2013 03:16:41
>>57289331
>Объяви раздел
Формальная верификация.

>определи H*
Логика Хоара.

>поясни первую строку
вывод по грамматике while-программ.

Втр 12 Ноя 2013 03:20:12
>>57289386
Теперь ты не узнаешь, кто твой батя.

Втр 12 Ноя 2013 03:30:32
>>57289486
Да и похуй.

Втр 12 Ноя 2013 03:32:57
>>57288949
говорила мама пидарасу малолетнему - учи лисп.

Втр 12 Ноя 2013 03:43:56
>>57289696
Это ты про ACL2? Попробую, спасибо.

Втр 12 Ноя 2013 04:02:45
>>57289427
Всё равно халява же. Ты сделал это упражнение и решил посмотреть, может ли двач в вывод формул, так ведь?
Алсо, там ведь можно сразу заменять высказывания на эквивалентные в соответствии с логикой высказываний?

Втр 12 Ноя 2013 04:07:04
>>57290132
>ты сделал это упражнение и решил посмотреть, может ли двач в вывод формул, так ведь?

Именно. К тому же хочу посмотреть есть ли более элегантное решение. У меня пиздец с 29-ю высказываниями учитывая импликации.

>Алсо, там ведь можно сразу заменять высказывания на эквивалентные в соответствии с логикой высказываний?
Можно. Но усиливать тройку можно только при помощи cons.

Втр 12 Ноя 2013 04:58:49
>>57290196
Мда. Хоть я и сказал "халява", я имел ввиду, что это халява для тебя - у меня есть только статья в википедии.
Я написал только для первой строчечки вывод, пытался что-то вразумительное для циклов написать, но там надо какие-то велосипеды с высказываниями изобретать, ну нах.
<x = X > 0 y = Y > 0 ^ 0 = 0> a:=0; <x = X > 0 y = Y ^ a = 0>
Ну хз, на первый взгляд правила вроде простые...

Втр 12 Ноя 2013 05:06:28
>>57290815
>но там надо какие-то велосипеды с высказываниями изобретать,
В них вся суть.

><x = X > 0 y = Y > 0 ^ 0 = 0> a:=0; <x = X > 0 y = Y ^ a = 0>
Аксиома присваивания применена верно, но постусловие для while не то. Лучше идти задом наперед и применять усиливание высказываний для слабых предусловий.

>Ну хз, на первый взгляд правила вроде простые...
Это да.

Втр 12 Ноя 2013 05:11:58
Подключи модуль math, crt; //ПЕТУХ!!


← К списку тредов