Re[25]: Жизнь без IDE
От: deniok Россия  
Дата: 01.11.09 11:40
Оценка:
Здравствуйте, Аноним, Вы писали:

А> Речь выше шла о тезисе, что средств формальной верификации для Java нет. Я же говорю, что таки есть.


Это средства формальной верификации аннотаций на JML к коду на Java. Сама Java недостаточно выразительна для верификации.
Re[15]: Жизнь без IDE
От: Аноним  
Дата: 01.11.09 11:56
Оценка:
Здравствуйте, Mr.Cat, Вы писали:

MC>Угу. Я иногда читаю чужой код и там бывает что-то такое:

MC>
MC>какаяТоФункция :: чтоТо -> НеведомаяМонада ЧтоТоЕще
MC>  ...
MC>

MC>Соответственно, хочется по минимуму бегать по гуглам и другим частям чужого исходника.

Leksah по Ctrl+double_click показывает тип функции + документацию из исходника + положение в дереве исходников. Оттуда по "go to definition" можно и на собственно исходники посмотреть (если GHC и библиотеки были поставлены с исходниками). Ну и автокомплит и подсветка и даже встроенный дебагер (GHCi) имеется.
Re[21]: Жизнь без IDE
От: thesz Россия http://thesz.livejournal.com
Дата: 01.11.09 15:55
Оценка:
Здравствуйте, Аноним, Вы писали:

А>Здравствуйте, thesz, Вы писали:


T>>Строгое формальное доказательство соответствия программ спецификации есть?


А>http://krakatoa.lri.fr/


Дорогой Аноним, вы уж и так напортачили, где только могли. Не стоит усугублять негативность отношения к вам ещё одним примером того, как плохо вы читаете комментарии, на которые собрались отвечать.

Чтобы вы поняли, на что надо отвечать: есть ли в языке Java формальное доказательство соответствия программ спецификации?

Так, чтобы ничего скачивать не пришлось.
Yours truly, Serguey Zefirov (thesz NA mail TOCHKA ru)
Re[22]: Жизнь без IDE
От: FR  
Дата: 06.11.09 13:07
Оценка:
Здравствуйте, thesz, Вы писали:

T>Чтобы вы поняли, на что надо отвечать: есть ли в языке Java формальное доказательство соответствия программ спецификации?


T>Так, чтобы ничего скачивать не пришлось.


Как я понял там только написанный на OCaml анализатор Java кода
Re[13]: Жизнь без IDE
От: xonixx  
Дата: 06.11.09 13:30
Оценка:
Здравствуйте, vshabanov, Вы писали:

V>У Хаскелла есть фундаментальное преимущество -- он чистый. Чистота опупительно повышает модульность.


А в лекции 5а SICP http://groups.csail.mit.edu/mac/classes/6.001/abelson-sussman-lectures/ почему-то утверждается строго противоположное!
sicp
Re[14]: Жизнь без IDE
От: vshabanov http://vshabanov-ru.blogspot.com
Дата: 06.11.09 14:52
Оценка:
Здравствуйте, xonixx, Вы писали:

X>Здравствуйте, vshabanov, Вы писали:


V>>У Хаскелла есть фундаментальное преимущество -- он чистый. Чистота опупительно повышает модульность.


X>А в лекции 5а SICP http://groups.csail.mit.edu/mac/classes/6.001/abelson-sussman-lectures/ почему-то утверждается строго противоположное!


Там утверждается, что чем больше глобальных переменных, тем лучше? Да, если в какой-то вложенный модуль надо передать какой-нить флажок logEnable, то может и стоит сделать его глобальным. Но это лучше вообще сделать через переменную окружения или -DDEBUG=1. Во всех остальных случаях, если алгоритм мутабельный и имеет внешние зависимости, то нельзя их прятать и создавать головную боль при поддержке. А когда язык тебе не позволяет прятать косяки под плющом, то сразу как-то по другому начинаешь проектировать, срубая ненужные зависимости, от чего имеешь феерический выигрыш на поддержке и очень малую цену изменения кода. Т.е. чистота в хаскеле мешает писать мутабельный/неявно связанный говонокод.
Re[15]: Жизнь без IDE
От: xonixx  
Дата: 06.11.09 15:10
Оценка:
Здравствуйте, vshabanov, Вы писали:

V>Здравствуйте, xonixx, Вы писали:


X>>Здравствуйте, vshabanov, Вы писали:


V>>>У Хаскелла есть фундаментальное преимущество -- он чистый. Чистота опупительно повышает модульность.


X>>А в лекции 5а SICP http://groups.csail.mit.edu/mac/classes/6.001/abelson-sussman-lectures/ почему-то утверждается строго противоположное!


V>Там утверждается, что чем больше глобальных переменных, тем лучше?


Нет, если точнее там говорилось ровно следующее

http://mitpress.mit.edu/sicp/full-text/sicp/book/node53.html

(Ctrl-F -> "While the program is still simple, it betrays some painful breaches of modularity")
Подождите ...
Wait...
Пока на собственное сообщение не было ответов, его можно удалить.