June 26th, 2017

Gen.Turgidson

Инварианты типа и зависимые типы

Кажется, кстати, в языках с всей этой наукой про пред- и пост- условия и проч. зависимые типы возникают естественным образом - в качестве ответа на потреность в инвариантах, зависящих от каких-то контекстных параметров:
  type array 'a model { length : int; mutable elts : map int 'a }
    invariant { 0 <= self.length }
val ([]) (a: array 'a) (i: int) : 'a
    requires { "expl:index in array bounds" 0 <= i < length a }
...

let  rev (len : int) (a : array 'a) (b : array 'a) 
      requires { a.length = len = b.length }
      ensures  { forall i : int . (0 <= i < len -> b [len - 1 - i] = a [i]) }
	=
      for i =  0 to len - 1 do
	invariant { forall k : int . (0 <= k < i -> b [len - 1 - k] = a [k]) } 
	b [len - 1 - i] <- a [i] 
      done
В общем-то поле length в типе array в данном коде лишнее и только мешает - например тем, что приходится доказывать условие a.length = len = b.length, которое в варианте вроде (если бы его язык допускал):
Collapse )
Gen.Turgidson

Так просто;

https://www.litmir.me/br/?b=549502&p=6
Жук. Не повредился он?
Жучиха. Что ты! Нетнет! Слава богу, нет. Уж как я перепугалась. Шарик мой миленький, не правда ли, ты целехонек? Ах… ты… ты… ты наша радость!
Жук. Гага, наш капиталец, наш навозик, наше золотце, наше… все!
Жучиха. Наш чудесный катышек, наш клад, наше сокровище, наше возлюбленное состояньице!
Жук. Наша любовь и единственная отрада! Уж как мы экономили и копили! Сколько навозу насобирали, вонючих катышков наберегли, во всем себе отказывали…
Жучиха. Сколько ходили, бродили, ножки намаяли, в дерьме рылись, пока мы тебя собрали да скатали…
Жук. …и закруглили, наше солнышко!
Жучиха. Наше сокровище!
Жук. Наша жизнь!
Жучиха. Дело всей нашей жизни!
Жук. Ты только понюхай, старая. Что за прелесть! Ты только прикинь, какой он увесистый.
Жучиха. Послалтаки господь!
Жук. Благословил нас...


© оба Чапека