Re: Design by contract
От: VladD2 Российская Империя www.nemerle.org
Дата: 06.06.11 15:30
Оценка: 8 (1)
Здравствуйте, artelk, Вы писали:

A>А возможно ли на Nemerle сделать "настоящий" Design by contract, со статической проверкой на вызывающей стороне?

A>Про эти макросы в курсе, но там проверка переносится в рантайм.

Где-то в сниппетах была версия которая работала с очень дремучей версией Spec#. Думаю даже начинающим не составит труда обернуть в макросы "Design by contract" API идущий с 4-ом фрэймвороком.

A>Единственное что приходит в голову, как это реализовать — это сделать, чтобы макросы requires/ensures делали из метода, для которого они указаны, макрос.


Зачем? В 4-ом фрэймворке есть контракты их и нужно использовать. Изменения будут тривиальны.

A>Но для этого потребуется такая фича как "макрос класса", по аналогии с "методом класса". Плюс нужна возможность использования макросов в той же сборке и возможность макросом сгенерировать определение другого макроса.


Макросы работают с типами описанными внутри проекта как с экземплярами класса TypeBuilder. Ничего специального для этого создавать не надо. Но как я уже говорил выше создавать инфраструктуру с нуля тоже нет смысла, так как в дотнете уже есть требуемая функциональность.
Есть логика намерений и логика обстоятельств, последняя всегда сильнее.
Re[2]: Design by contract
От: WolfHound  
Дата: 07.06.11 08:28
Оценка: 3 (1)
Здравствуйте, Denom, Вы писали:

D>А есть вообще где либо (в каком либо языке) Design by Contract со статической проверкой?

Контракты фигня по сравнению с этим:
http://en.wikipedia.org/wiki/Dependent_type
... << RSDN@Home 1.2.0 alpha 4 rev. 1472>>
Пусть это будет просто:
просто, как только можно,
но не проще.
(C) А. Эйнштейн
Design by contract
От: artelk  
Дата: 06.06.11 13:58
Оценка: 1 (1)
А возможно ли на Nemerle сделать "настоящий" Design by contract, со статической проверкой на вызывающей стороне?
Про эти макросы в курсе, но там проверка переносится в рантайм.
Единственное что приходит в голову, как это реализовать — это сделать, чтобы макросы requires/ensures делали из метода, для которого они указаны, макрос.
И чтобы "вызов" этого метода-макроса был бы триггером для отработки соответствующей логики проверки на вызывающей стороне и выполняемой в компайл-тайм.
Но для этого потребуется такая фича как "макрос класса", по аналогии с "методом класса". Плюс нужна возможность использования макросов в той же сборке и возможность макросом сгенерировать определение другого макроса.

1. Какие идеи на этот счет?
2. Будут ли такие возможности в N2?
Re[2]: Design by contract
От: BogdanMart Украина  
Дата: 06.06.11 22:54
Оценка:
Здравствуйте, VladD2, Вы писали:

A>>Но для этого потребуется такая фича как "макрос класса", по аналогии с "методом класса". Плюс нужна возможность использования макросов в той же сборке и возможность макросом сгенерировать определение другого макроса.


VD>Макросы работают с типами описанными внутри проекта как с экземплярами класса TypeBuilder. Ничего специального для этого создавать не надо. Но как я уже говорил выше создавать инфраструктуру с нуля тоже нет смысла, так как в дотнете уже есть требуемая функциональность.


Полагаю это нечто типа продвинутого АОП.

Т.е. сборка инсталит некий хук который будет вызван в случае обращения к методам/данным в ней объявленным. (т.е. без навешивания макроса уровня сборки, а автоматом) Хотя, наверно, слишком геморно.
Re[2]: Design by contract
От: artelk  
Дата: 07.06.11 06:29
Оценка:
Здравствуйте, VladD2, Вы писали:

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


A>>А возможно ли на Nemerle сделать "настоящий" Design by contract, со статической проверкой на вызывающей стороне?

A>>Про эти макросы в курсе, но там проверка переносится в рантайм.

VD>Где-то в сниппетах была версия которая работала с очень дремучей версией Spec#. Думаю даже начинающим не составит труда обернуть в макросы "Design by contract" API идущий с 4-ом фрэймвороком.


Спасибо, только вопрос был не в стиле "хочу прикрутить фичу, помогите", а просто из любопытства .
Nemerle позиционируется как язык, в котором недостающие языковые фичи можно реализовать макросами.
Вот и хотелось бы узнать до каких границ это так.

A>>Единственное что приходит в голову, как это реализовать — это сделать, чтобы макросы requires/ensures делали из метода, для которого они указаны, макрос.


VD>Зачем? В 4-ом фрэймворке есть контракты их и нужно использовать. Изменения будут тривиальны.


Да, но N2 не будет прибит гвоздями к .NET. Или я не прав?

A>>Но для этого потребуется такая фича как "макрос класса", по аналогии с "методом класса". Плюс нужна возможность использования макросов в той же сборке и возможность макросом сгенерировать определение другого макроса.


VD>Макросы работают с типами описанными внутри проекта как с экземплярами класса TypeBuilder. Ничего специального для этого создавать не надо. Но как я уже говорил выше создавать инфраструктуру с нуля тоже нет смысла, так как в дотнете уже есть требуемая функциональность.


Ага, т.е. использовать внешние тулзы. В дотнете есть и t4, так что, макросы не нужны чтоли?
Re: Design by contract
От: Denom Украина  
Дата: 07.06.11 07:55
Оценка:
Здравствуйте, artelk, Вы писали:

A>А возможно ли на Nemerle сделать "настоящий" Design by contract, со статической проверкой на вызывающей стороне?

А есть вообще где либо (в каком либо языке) Design by Contract со статической проверкой?
... << RSDN@Home 1.2.0 alpha 4 rev. 1476>>
Re[3]: Design by contract
От: Denom Украина  
Дата: 07.06.11 12:03
Оценка:
Здравствуйте, WolfHound, Вы писали:

WH>Контракты фигня по сравнению с этим:

WH>http://en.wikipedia.org/wiki/Dependent_type

Про зависимые типы читал, это все понятно.
Для этого, как мне кажется, нужно кардинально менять систему типов.
Наверное прийдётся гарантировать чистоту функций, явно вводить монады...
А все-таки: именно контракты где-нибудь реализованы в статике (не в чисто функциональных языках типа agda )?
... << RSDN@Home 1.2.0 alpha 4 rev. 1476>>
Re[4]: Design by contract
От: WolfHound  
Дата: 07.06.11 12:20
Оценка:
Здравствуйте, Denom, Вы писали:

D>А все-таки: именно контракты где-нибудь реализованы в статике (не в чисто функциональных языках типа agda )?

Так _один_ клик с той страницы ссылку на которую я дал.
{n:nat}
int bsearch(key: int, vec[n]: int) {
  var: int low, mid, high;
       int x;;

  low = 0; high = arraysize(vec) - 1;

  invariant:
    [i:int, j:int | 0 <= i <= n, 0 <= j+1 <= n] (low: int(i), high: int(j))
  while (low <= high) {
    mid = (low + high) / 2;
    x = vec[mid];
    if (key == x) { return mid; }
    else if (key < x) { high = mid - 1; }
         else { low = mid + 1; }
  }
  return -1;
}

(С) http://www.cs.bu.edu/~hwxi/Xanadu/Xanadu.html
... << RSDN@Home 1.2.0 alpha 4 rev. 1472>>
Пусть это будет просто:
просто, как только можно,
но не проще.
(C) А. Эйнштейн
Re[5]: Design by contract
От: Denom Украина  
Дата: 07.06.11 12:43
Оценка:
Здравствуйте, WolfHound, Вы писали:

Т.е инвариант реализован через зависимые типы?
Это часть библиотеки (redefined dependent type) или реализован в компиляторе?
... << RSDN@Home 1.2.0 alpha 4 rev. 1476>>
Re[5]: Design by contract
От: Denom Украина  
Дата: 07.06.11 12:45
Оценка:
Здравствуйте, WolfHound, Вы писали:

Зависимые типы реально реализовать на макросах, не трогая компилятор?
... << RSDN@Home 1.2.0 alpha 4 rev. 1476>>
Re[3]: Design by contract
От: VladD2 Российская Империя www.nemerle.org
Дата: 07.06.11 13:34
Оценка:
Здравствуйте, artelk, Вы писали:

A>Спасибо, только вопрос был не в стиле "хочу прикрутить фичу, помогите", а просто из любопытства .

A>Nemerle позиционируется как язык, в котором недостающие языковые фичи можно реализовать макросами.
A>Вот и хотелось бы узнать до каких границ это так.

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

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

A>Да, но N2 не будет прибит гвоздями к .NET. Или я не прав?


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

A>Ага, т.е. использовать внешние тулзы. В дотнете есть и t4, так что, макросы не нужны чтоли?


Причем тут Т4? Если есть готовое решение вроде дотнетных контрактов, то макросы позволят за считанные часа реализовать для них красивый синтаксис. Если готового решения нет, или по каким-то причинам его не хочется использовать, то кроме синтаксиса придется реализовать и всю логику этих самых контрактов. А это, между нами девочками, научная работа уровня докторского дисера.

Если тебе очень хочется — можешь заняться разработкой своего варианта. Но учти что это задача на много лет.
Есть логика намерений и логика обстоятельств, последняя всегда сильнее.
 
Подождите ...
Wait...
Пока на собственное сообщение не было ответов, его можно удалить.