* [sisyphus] I: new package
@ 2003-03-16 0:44 Vitaly Lugovsky
2003-03-16 8:43 ` Pavel S. Khmelinsky
0 siblings, 1 reply; 4+ messages in thread
From: Vitaly Lugovsky @ 2003-03-16 0:44 UTC (permalink / raw)
To: devel; +Cc: sisyphus
why-1.05-alt1.src.rpm ушёл в incoming.
Это средство для автоматического доказательства аннотированных
программ (т.е. спецификация идёт внутри кода, а не отдельными
утверждениями), работает поверх Coq (и некоторых других
proof-assistant-ов). Понимает некоторое подмножество языка C (без
арифметики указателей) и подмножество Caml (без type inferrence,
и т.п.)
A must have для любого уважающего себя программиста. Давайте
писать доказанно безошибочный код, и побольше!
В ближайшее время в Сизиф пойдёт и система Krokatoa для
доказательства аннотированного Java-кода.
^ permalink raw reply [flat|nested] 4+ messages in thread
* Re: [sisyphus] I: new package
2003-03-16 0:44 [sisyphus] I: new package Vitaly Lugovsky
@ 2003-03-16 8:43 ` Pavel S. Khmelinsky
2003-03-17 0:14 ` Vitaly Lugovsky
0 siblings, 1 reply; 4+ messages in thread
From: Pavel S. Khmelinsky @ 2003-03-16 8:43 UTC (permalink / raw)
To: sisyphus
Vitaly Lugovsky wrote:
>писать доказанно безошибочный код, и побольше!
>
> В ближайшее время в Сизиф пойдёт и система Krokatoa для
>доказательства аннотированного Java-кода.
>
>
А что такое "аннотированный"?
^ permalink raw reply [flat|nested] 4+ messages in thread
* Re: [sisyphus] I: new package
2003-03-16 8:43 ` Pavel S. Khmelinsky
@ 2003-03-17 0:14 ` Vitaly Lugovsky
2003-03-17 18:14 ` Pavel S. Khmelinsky
0 siblings, 1 reply; 4+ messages in thread
From: Vitaly Lugovsky @ 2003-03-17 0:14 UTC (permalink / raw)
To: sisyphus
On Sun, 16 Mar 2003, Pavel S. Khmelinsky wrote:
> >писать доказанно безошибочный код, и побольше!
> >
> > В ближайшее время в Сизиф пойдёт и система Krokatoa для
> >доказательства аннотированного Java-кода.
> >
> >
> А что такое "аннотированный"?
Комментарии к коду содержат констрейны (e.g., что такой-то
параметр всегда больше нуля, что переменная x обязана быть больше
суммы y и z, ну и т.п.).
В качестве примера в Why было доказательство оптимальности
алгоритма Бейзенхема, рекомендую ознакомиться.
^ permalink raw reply [flat|nested] 4+ messages in thread
* Re: [sisyphus] I: new package
2003-03-17 0:14 ` Vitaly Lugovsky
@ 2003-03-17 18:14 ` Pavel S. Khmelinsky
0 siblings, 0 replies; 4+ messages in thread
From: Pavel S. Khmelinsky @ 2003-03-17 18:14 UTC (permalink / raw)
To: sisyphus
Vitaly Lugovsky wrote:
>On Sun, 16 Mar 2003, Pavel S. Khmelinsky wrote:
>
>
>
>>>писать доказанно безошибочный код, и побольше!
>>>
>>>В ближайшее время в Сизиф пойдёт и система Krokatoa для
>>>доказательства аннотированного Java-кода.
>>>
>>>
>>>
>>>
>>А что такое "аннотированный"?
>>
>>
>
> Комментарии к коду содержат констрейны (e.g., что такой-то
>параметр всегда больше нуля, что переменная x обязана быть больше
>суммы y и z, ну и т.п.).
>
> В качестве примера в Why было доказательство оптимальности
>алгоритма Бейзенхема, рекомендую ознакомиться.
>
>
Понял, спасибо за разъяснение.
>
>_______________________________________________
>Sisyphus mailing list
>Sisyphus@altlinux.ru
>http://altlinux.ru/mailman/listinfo/sisyphus
>
>
>
>
^ permalink raw reply [flat|nested] 4+ messages in thread
end of thread, other threads:[~2003-03-17 18:14 UTC | newest]
Thread overview: 4+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2003-03-16 0:44 [sisyphus] I: new package Vitaly Lugovsky
2003-03-16 8:43 ` Pavel S. Khmelinsky
2003-03-17 0:14 ` Vitaly Lugovsky
2003-03-17 18:14 ` Pavel S. Khmelinsky
ALT Linux Sisyphus discussions
This inbox may be cloned and mirrored by anyone:
git clone --mirror http://lore.altlinux.org/sisyphus/0 sisyphus/git/0.git
# If you have public-inbox 1.1+ installed, you may
# initialize and index your mirror using the following commands:
public-inbox-init -V2 sisyphus sisyphus/ http://lore.altlinux.org/sisyphus \
sisyphus@altlinux.ru sisyphus@altlinux.org sisyphus@lists.altlinux.org sisyphus@lists.altlinux.ru sisyphus@lists.altlinux.com sisyphus@linuxteam.iplabs.ru sisyphus@list.linux-os.ru
public-inbox-index sisyphus
Example config snippet for mirrors.
Newsgroup available over NNTP:
nntp://lore.altlinux.org/org.altlinux.lists.sisyphus
AGPL code for this site: git clone https://public-inbox.org/public-inbox.git