mod Ex03a

incl Mtex

incl Mtexln

incl Maux

loc rem 
  \para \bf  3. CVIČENIE Z PREDMETU 1-AIN-470 ŠPECIFIKÁCIA A VERIFIKÁCIA 
  PROGRAMOV  \end 

loc rem 
  \para* \it  Meno:  \end 
  \para* \it  Verzia CL:  \end 5.81.21.2 
  \para* \it  Dátum:  \end pondelok 27.2.2023 
  \para* \it  WWW:  \end 
  http://www.ii.fmph.uniba.sk/cl/view.php/courses/1-AIN-470-svp/2223ls/?lang=sk 
  \para* \it  Kontakt:  \end Jan.Komara(at)fmph.uniba.sk 

loc rem 
  \para \bf  Úvodná poznámka.  \end Toto cvičenie je venované týmto 
  témam: 
  \items 
   \item \para celočíselná odmocnina (názorný príklad), 
   \item \para Cantorova párovacia funkcia a aritmetizácia karteziánskeho 
         súčinu, 
   \item \para Catalanova párovacia funkcia. 
  \end
  \para Zadanie sa skladá z týchto súborov: 
  \items 
   \item \para Súbory \it  mtex*.cl  \end obsahujú makrá pre CL-TeX. 
   \item \para Súbory \it  maux*.cl  \end obsahujú definície a vlastnosti 
         pomocných funkcií a predikátov. 
   \item \para Súbory \it  ex*.cl  \end obsahujú úlohy, ktoré máte riešiť 
         na tomto cvičení. 
   \item \para Súbor \it  msyntax.cl  \end obsahuje základnú syntax systému 
         CL. 
  \end
  \para Tieto súbory sa musia skompilovať v správnom poradí. Presný postup 
  je uvedený v súbore \it  readme.txt  \end. 

loc rem 
  \para \bf  Hodnotenie.  \end 
  \items 
   \item \para Počet bodov za úlohy v tomto súbore: 2 
   \item \para Počet bodov za prémiove úlohy v tomto súbore: 0 
  \end
  \para Odovzdať do 4.3.2023 (sobota). 

loc rem 
  ******************************************************************************
  ********************************* EXERCISES **********************************
  ******************************************************************************

rem 
  \para \bf  Literature.  \end 
  \items 
   \item \para \it  [1]  \end J. Komara. Specification and Verification of 
         Programs. Online. 
   \item \para \it  [2]  \end Ján Kľuka. Úvod do deklaratívneho 
         programovania. Online. 
   \item \para \it  [3]  \end Ján Komara. Recursive Functions. Online. 
  \end

rem 
  \para \bf  [CL] Remark.  \end Catalan pairing function - see the module \it  
  Maux*  \end. 

rem 
  \para \bf  Chapter. Programs Operating on Lists.  \end 

rem 
  \para \bf  Section. Lists.  \end 

rem 
  \para \bf  [CL] Formatting the output.  \end Use the format \ft Ln \end to 
  display numbers in the list representation. For instance, the result of the 
  query \ft '147775=xs:Ln' \end is shown as the expression \ft 1,2,3,4,0 \end. 
  Note that the predicate \ft Ln \end is defined in the module \it  Standard 
   \end. 

rem 
  \para \bf  List length.  \end 

fun L 
  L(0) = 0
  L(x,xs) = L(xs)+1

rem 
  \para \bf  List indexing.  \end 

fun/2 Sub 'Tex_f2_ln_sub'
  Sub(xs,i) = Proj1 Iproj2(i,xs)

rem 
  \para \bf  [CL] List membership.  \end The list membership predicate 
  \ft x in xs \end is defined in the module \it  Standard  \end: 
  \eq* 
    x in xs <-> \e i(i < L(xs) & x = Sub(xs,i))
  \end
  \para \it  Notation.  \end We write \ft 'x in xs' \end for the application 
  \ft x in xs \end and \ft 'x !in xs' \end for its negation \ft x !in xs \end. 

rem 
  \para \bf  List concatenation.  \end Define the function \ft x++y \end such 
  that 
  \eq* 
    xs++ys = zs <-> 
    L(zs) = L(xs)+L(ys) & \a i(i < L(xs) -> Sub(zs,i) = Sub(xs,i)) & 
    \a i(i < L(xs) -> Sub(zs,L(xs)+i) = Sub(ys,i))
  \end

fun/2 Conc 'Tex_f2_ln_conc'
  Conc(xs,ys) = Foo

rem 
  \para \bf  [CL] Remark.  \end The list concatenation function \ft xs++ys \end, 
  written as \ft 'xs ++ ys' \end, is defined in the module \it  Standard  \end. 

rem 
  \para \bf  List reversal.  \end \header* fun Rev 'Tex_f1_ln_rev' \end Define 
  the function \ft Rev(xs) \end such that 
  \eq* 
    Rev(xs) = ys <-> 
    L(ys) = L(xs) & \a i(i < L(xs) -> Sub(ys,i) = Sub(xs,L(ys)-(i+1)))
  \end

fun Rev 'Tex_f1_ln_rev'
  Rev(xs) = Foo

rem 
  \para \bf  Fast reversal. \it  (1 point)  \end  \end Find an efficient 
  implementation of the list reversal function. 

fun/2 Reva 'Tex_f2_f'
  Reva(xs,as) = Foo

rem 
  \para Invariant 
  \eq* 
    Reva(xs,as) = Rev(xs)++as
  \end

fun Rev_by_reva 'Tex_f1_ln_rev'
  Rev_by_reva(xs) = Foo

rem 
  \para \bf  Section. Operations on Lists.  \end 

rem 
  \para \bf  List modification.  \end \header* fun/3 Msub 'Tex_f3_ln_msub' \end 
  Define the function \ft Msub(xs,i,a) \end such that 
  \eq* 
    i < L(xs) -> L Msub(xs,i,a) = L(xs)
  \end
  \eq* 
    i < L(xs) -> Sub(Msub(xs,i,a),i) = a
  \end
  \eq* 
    i < L(xs) & j < L(xs) & j != i -> Sub(Msub(xs,i,a),j) = Sub(xs,j)
  \end

fun/3 Msub 'Tex_f3_ln_msub'
  Msub(xs,i,a) = Foo

rem 
  \para \bf  Map.  \end 

theory Theory_map

fun F 'Tex_f1_f'

rem 
  \para \header* fun Map 'Tex_f1_ln_map_f' \end Define the function 
  \ft Map(xs) \end such that 
  \eq* 
    L Map(xs) = L(xs)
  \end
  \eq* 
    i < L(xs) -> Sub(Map(xs),i) = F Sub(xs,i)
  \end

fun Map 'Tex_f1_ln_map_f'
  Map(xs) = Foo

end theory Theory_map

rem 
  \para \bf  Zip and unzip.  \end \header* fun/2 Zip  \end Define the functions 
  \ft Zip(xs,ys) \end and \ft Unzip(zs) \end such that 
  \eq* 
    L(xs) = L(ys) -> L Zip(xs,ys) = L(xs)
  \end
  \eq* 
    L(xs) = L(ys) & i < L(xs) -> Sub(Zip(xs,ys),i) = Sub(xs,i),Sub(ys,i)
  \end
  \para and 
  \eq* 
    L(xs) = L(ys) -> Unzip Zip(xs,ys) = xs,ys
  \end

fun/2 Zip 
  Zip(xs,ys) = Foo

fun Unzip 
  Unzip(zs) = Foo

rem 
  \para \bf  Interval.  \end 
  \header* fun/2 Interval 'Tex_f2_ln_interval_co' \end Define the function 
  \ft Interval(m,n) \end such that 
  \eq* 
    m <= n -> L Interval(m,n) = n-m
  \end
  \eq* 
    m+i < n -> Sub(Interval(m,n),i) = m+i
  \end

fun/2 Interval 'Tex_f2_ln_interval_co'
  Interval(m,n) = Foo

rem 
  \para \bf  Elements with even and odd indices.  \end Define the functions 
  \ft Ieven(xs) \end and \ft Iodd(xs) \end such that 
  \eq* 
    L Ieven(xs) = (L(xs)+1)/2
  \end
  \eq* 
    2*i < L(xs) -> Sub(Ieven(xs),i) = Sub(xs,2*i)
  \end
  \para and 
  \eq* 
    L Iodd(xs) = L(xs)/2
  \end
  \eq* 
    2*i+1 < L(xs) -> Sub(Iodd(xs),i) = Sub(xs,2*i+1)
  \end
  \para \it  Hint.  \end Use the following discrimination: 
  \def 
    fun F 'Tex_f1_f'
    F(0) = Foo
    F(x,0) = Foo
    F(x,y,zs) = Foo
  \end

fun Ieven 
  Ieven(xs) = Foo

fun Iodd 
  Iodd(xs) = Foo

rem 
  \para \bf  Combining two lists.  \end \header* fun/2 Combine  \end Define the 
  function \ft Combine(xs,ys) \end such that 
  \eq* 
    Combine(Ieven(xs),Iodd(xs)) = xs
  \end

fun/2 Combine 
  Combine(xs,ys) = Foo

rem 
  \para \bf  Take and drop.  \end \header* fun/2 Take  \end 
  \header* fun/2 Drop  \end Define the functions \ft Take(n,xs) \end and 
  \ft Drop(n,xs) \end such that 
  \eq* 
    n <= L(xs) -> L Take(n,xs) = n
  \end
  \eq* 
    n <= L(xs) -> \e ys xs = Take(n,xs)++ys
  \end
  \para and 
  \eq* 
    n <= L(xs) -> L Drop(n,xs) = L(xs)-n
  \end
  \eq* 
    n <= L(xs) -> \e ys xs = ys++Drop(n,xs)
  \end

fun/2 Take 
  Take(n,xs) = Foo

fun/2 Drop 
  Drop(n,xs) = Foo

rem 
  \para \bf  Minimum and maximum of lists.  \end Define the functions 
  \ft Minl(xs) \end and \ft Maxl(xs) \end such that 
  \eq* 
    xs != 0 -> Minl(xs) in xs
  \end
  \eq* 
    xs != 0 & a in xs -> Minl(xs) <= a
  \end
  \para and 
  \eq* 
    xs != 0 -> Maxl(xs) in xs
  \end
  \eq* 
    xs != 0 & a in xs -> a <= Maxl(xs)
  \end

fun Minl 
  Minl(xs) = Foo

fun Maxl 
  Maxl(xs) = Foo

rem 
  \para \bf  Deleting elements from lists.  \end \header* fun/2 Delall  \end 
  Define the function \ft Delall(a,xs) \end such that 
  \eq* 
    b in Delall(a,xs) <-> b in xs & b != a
  \end

fun/2 Delall 
  Delall(a,xs) = Foo

rem 
  \para \bf  Filter.  \end 

theory Theory_filter

pred A 

rem 
  \para \header* fun Filter 'Tex_f1_ln_filter_a' \end Define the function 
  \ft Filter(xs) \end such that 
  \eq* 
    a in Filter(xs) <-> a in xs & A(a)
  \end

fun Filter 'Tex_f1_ln_filter_a'
  Filter(xs) = Foo

end theory Theory_filter

rem 
  \para \bf  Counting the number of occurrences in lists.  \end 
  \header* fun/2 Count 'Tex_f2_ln_count' \end Define the function 
  \ft Count(a,x) \end such that 
  \eq* 
    Count(a,b,0) = Eqf(a,b)
  \end
  \eq* 
    Count(a,xs++ys) = Count(a,xs)+Count(a,ys)
  \end
  \para The \ft Eqf(x,y) \end is the characteristic function of the binary 
  equality predicate \ft x = y \end and it is defined in the module \it  Maux* 
   \end. 

fun/2 Count 'Tex_f2_ln_count'
  Count(a,xs) = Foo

rem 
  \para \bf  Removal of duplicates from lists.  \end Define the function 
  \ft Nodoubles(xs) \end such that 
  \eq* 
    a in Nodoubles(xs) <-> a in xs
  \end
  \eq* 
    a in Nodoubles(xs) -> Count(a,Nodoubles(xs)) = 1
  \end

fun Nodoubles 
  Nodoubles(xs) = Foo

rem 
  \para \bf  Union list. \it  (1 point)  \end  \end 
  \header* fun Union 'Tex_f1_ln_union' \end Define the function 
  \ft Union(xss) \end such that 
  \eq* 
    Union(xs,0) = xs
  \end
  \eq* 
    Union(xss++yss) = Union(xss)++Union(yss)
  \end

fun Union 'Tex_f1_ln_union'
  Union(xss) = Foo

