kouzdra (kouzdra) wrote,
kouzdra
kouzdra

This journal has been placed in memorial status. New entries cannot be posted to it.

Category:

По поводу призраков:

Кажется не все въезжают, "о чем это":
ghost var prevElements := a[..];
while // ...
  invariant a[lo..hi] == prevElements[lo..hi];
{
  // ...
}
ghost var нужны имено для задания инвариантов без порождения лишнего кода. С точки зрения компилятора они ведут так же как обычные и на общих правах участвую в процессе верификации "как если бы были настоящими" - но в код это не попадает.

Аналогом этого кода в С было бы что-то вроде:
  std::vector<int> a = ...
  ...
  auto const inv = std::vector<int> (a [lo], a [hi]);
  for (int i = 0; i != a.size(); ++ i) {
    assert (inv == std::vector<int> (a [lo], a [hi]));
    ...
  }
Только без оверхеда и с контролем условия во время компиляции
Tags: dafny, verification, Компутерщина, Языки программирования
Subscribe

  • "И все его оставили"

    Чего0то мне кажется, что на Украине жизнь скоро может начать иллюстрировать искусство: Когда случился тот неслыханный скандал, тот крик, и брань, и…

  • Технологии

    "... держать молоток либо какие-то новые технологии...", – считает Володин.

  • Попались обсуждения какого-то

    гопнического сериала про "слова пацанов", там в воспоминательных рассуждаловах всякие личные воспоминание про "с раёнов" - поражает театраьность и…

  • Post a new comment

    Error

    Comments allowed for friends only

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 3 comments