| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/structures/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quellcode-Bibliothek array2list.pvs Sprache: PVS |
|||||||||
|
array2list[T:TYPE+] : THEORY
BEGIN IMPORTING listn[T], more_list_props array2list_it(a:[nat->T],n:nat,i:upto(n)) : RECURSIVE {l:listn(n-i) | FORALL (j:subrange(i,n-1)) : a(j) = nth(l,j-i)} = IF i = n THEN null ELSE cons(a(i),array2list_it(a,n,i+1)) ENDIF MEASURE n-i array2list(n:nat)(a:[nat->T]) : {l:listn(n) | FORALL (i:below(n)) : a(i) = nth(l,i)} = array2list_it(a,n,0) list2array(t:T)(l:list)(i:nat) : RECURSIVE T = IF null?(l) THEN t ELSIF i=0 THEN car(l) ELSE list2array(t)(cdr(l))(i-1) ENDIF MEASURE l BY << list2array_sound : LEMMA FORALL(l:list,t:T,i:nat) : list2array(t)(l)(i) = IF i < length(l) THEN nth(l,i) ELSE t ENDIF default : T = choose({t:T|true}) list2array_default(l:list) : MACRO [nat->T] = list2array(default)(l) array2list_inv : LEMMA FORALL (a:[nat->T],t:T,n:nat,i:below(n)) : list2array(t)(array2list(n)(a))(i) = a(i) list2array_inv : LEMMA FORALL (l:list,t:T,i:below(length(l))) : nth(array2list(length(l))(list2array(t)(l)),i) = nth(l,i) list2array_inv_ext : LEMMA FORALL (l:list,t:T) : array2list(length(l))(list2array(t)(l)) = l fill(t:T,n:nat) : {l:listn(n) | FORALL (i:below(n)) : nth(l,i) = t} = array2list(n)(LAMBDA(n:nat):t) END array2list ¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.11Bemerkung: (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28