Quelle  fseqs_aux_2D.pvs

fseqs_aux_2D[gsmin,gsmax:posreal] : THEORY
BEGIN

  IMPORTING structures@sort_fseq[real,<=],
     structures@fseqs_ops[real],
            trig_fnd@to2pi

  vs,fs   : VAR fseq

  %%%%% Track Angle %%%%%

  trk_fseq?(fs): bool = 
    FORALL (i:below(fs`length)): 0 <= fs`seq(i) AND fs`seq(i) <= 2*pi 

  empty_trk_fseq : JUDGEMENT
    emptyseq HAS_TYPE (trk_fseq?)

  trkb,trkb1,trkb2 : VAR (trk_fseq?)

  comp_trk_fseq : JUDGEMENT
    o(trkb1,trkb2) HAS_TYPE (trk_fseq?)

  sort_trk_fseq : JUDGEMENT
    sort(trkb) HAS_TYPE (trk_fseq?)

  %%%%% Ground Speed %%%%%

  gs_fseq?(fs) : bool = 
    FORALL (i:below(fs`length)): gsmin<=fs`seq(i) AND fs`seq(i)<=gsmax

 gsb,gsb1,gsb2 : VAR (gs_fseq?)

  empty_gs_fseq : JUDGEMENT
    emptyseq HAS_TYPE (gs_fseq?)

  comp_gs_fseq : JUDGEMENT
    o(gsb1,gsb2) HAS_TYPE (gs_fseq?)

  sort_gs_fseq : JUDGEMENT
    sort(gsb) HAS_TYPE (gs_fseq?)


END fseqs_aux_2D