Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: numerical_bandb.pvs Sprache: PVS

Original von: PVS^©

numerical_bandb : THEORY
BEGIN

  IMPORTING safe_arith,
            interval_expr,
            structures@array2list[real],
            structures@Maybe,
            reals@real_orders

  IntervalMinMax : TYPE = [#
    mm     : Interval,
    lb_max : real,
    lb_box : ProperBox,
    ub_min : real,
    ub_box : ProperBox
  #]

  IMPORTING structures@branch_and_bound[RealExpr,IntervalMinMax,ProperBox,nat]

  v         : VAR nat
  maxdepth  : VAR nat
  expr      : VAR RealExpr
  box       : VAR ProperBox
  dirvar    : VAR DirVar
  dirvars   : VAR DirVarStack
  M,M1,M2   : VAR IntervalMinMax
  out       : VAR Output
  precision : VAR posreal
  prune,ge  : VAR ExitPred
  le        : VAR LocalExitPred
  select    : VAR DirVarSelector
  acc       : VAR IntervalMinMax

  evaluate(box,expr) : IntervalMinMax =
    LET X   = Eval(expr,box),
        Lb  = Lbbox(box),
        Ub  = Ubbox(box),
        P1  = Eval(expr,Lb),
        P2  = Eval(expr,Ub),
        (lb_max,lb_box) = IF ub(P1) < ub(P2) THEN (ub(P1),Lb) ELSE (ub(P2),Ub) ENDIF,
        (ub_min,ub_box) = IF lb(P1) > lb(P2) THEN (lb(P1),Lb) ELSE (lb(P2),Ub) ENDIF IN
    (# mm     := X,
       lb_max := lb_max,
       lb_box := lb_box,
       ub_min := ub_min,
       ub_box := ub_box
    #)

  branch(v,expr) : [RealExpr,RealExpr] = (expr,expr)
  denorm(dirvar,M) : IntervalMinMax = M

  combine(v,M1,M2) : IntervalMinMax =
    LET M_lb = IF M1`lb_max < M2`lb_max THEN M1 ELSE M2 ENDIF,
        M_ub = IF M1`ub_min > M2`ub_min THEN M1 ELSE M2 ENDIF IN
    (# mm     := Safe2(Union)(mm(M1),mm(M2)),
       lb_max := M_lb`lb_max,
       lb_box := M_lb`lb_box,
       ub_min := M_ub`ub_min,
       ub_box := M_ub`ub_box #)

  % <= 0 : min
  % >= 0 : max
  min_or_max: VAR int

  prune_mm(min_or_max)(dirvars,acc,M) : bool =
    (min_or_max <= 0 IMPLIES acc`lb_max <= lb(M`mm)) AND
    (min_or_max >= 0 IMPLIES ub(M`mm) <= acc`ub_min)

  le_mm(min_or_max,precision)(M) : bool =
    (min_or_max <= 0 IMPLIES LET lb = M`lb_max - lb(M`mm) IN lb <= precision) AND
    (min_or_max >= 0 IMPLIES LET ub = ub(M`mm) - M`ub_min IN ub <= precision)

  ge_mm(dirvars,acc,M) : bool = EmptyInterval?(M`mm)

  accumulate(acc,M) : IntervalMinMax =
    combine(0,acc,M)

  subdivide(v,box) : [ProperBox,ProperBox] = split(v,box)

  VarSel : TYPE = [# thisvar: nat, lb: real, ub: real, lbub: Interval #]

  var_varsel(expr:RealExpr,box:ProperBox,both:bool,
             Mb:listn[Interval](length(box)))
            (v:below(length(box))) : VarSel =
    LET X    = nth(box,v),
     lb   = IF both THEN lb(Eval(expr,setnth(Mb,v,LAMBDA(x:Interval): [| lb(X) |]))) ELSE 0 ENDIF,
     ub   = IF both THEN ub(Eval(expr,setnth(Mb,v,LAMBDA(x:Interval): [| ub(X) |]))) ELSE 0 ENDIF,
lbub = Eval(expr,setnth(Mb,v,LAMBDA(x:Interval):X)) IN
    (# thisvar  := v,
       lb       := lb,
       ub       := ub,
       lbub     := lbub
     #)

  max_varsel(vs1,vs2:VarSel) : VarSel =
    IF size(vs1`lbub) > size(vs2`lbub) THEN vs1
    ELSE vs2
    ENDIF

  IMPORTING structures@for_iterate

  both, dir : VAR bool

  mindir_maxvar_aux(both:bool)(dirvars,acc,box,expr) : DirVar =
    IF length(box) <= 1 THEN left(0)
    ELSE
      LET Mb = Midbox(box),
          vs = iterate_left(0,length(box)-1,var_varsel(expr,box,both,Mb),max_varsel) IN
      (vs`lb < vs`ub,vs`thisvar)
    ENDIF

  mindir_maxvar(dirvars,acc,box,expr) : DirVar =
    mindir_maxvar_aux(TRUE)(dirvars,acc,box,expr)

  maxdir_maxvar(dirvars,acc,box,expr) : DirVar =
    LET (dir,v) = mindir_maxvar(dirvars,acc,box,expr) IN
    (NOT dir,v)

  altdir_maxvar(dirvars,acc,box,expr) : DirVar =
    LET (dir,v) = mindir_maxvar_aux(FALSE)(dirvars,acc,box,expr) IN
      (even?(length(dirvars)),v)

  dir_maxvar(dir)(dirvars,acc,box,expr) : DirVar =
    LET v = mindir_maxvar_aux(FALSE)(dirvars,acc,box,expr)`2 IN
      (dir,v)

  max_rec(n:posnat,m:real,v:below(n),
                 i:subrange(1,n),b:Box | n = length(b)+i) : RECURSIVE below(n) =
    IF null?(b) THEN v
    ELSE LET mm = size(car(b)) IN
           IF mm > m THEN max_rec(n,mm,i,i+1,cdr(b))
           ELSE max_rec(n,m,v,i+1,cdr(b))
           ENDIF
    ENDIF
  MEASURE b BY <<

  max_aux(box) : nat =
    IF length(box) <= 1 THEN 0
    ELSE max_rec(length(box),size(car(box)),0,1,cdr(box))
    ENDIF

  dir_max(dir)(dirvars,acc,box,expr) : DirVar =
    (dir,max_aux(box))

  alt_max(dirvars,acc,box,expr) : DirVar =
    (even?(length(dirvars)),max_aux(box))

  altvar(dirvars,box) : nat =
    IF length(box) <= 1 THEN 0
    ELSE mod(length(dirvars),length(box))
    ENDIF

  dir_alt(dir)(dirvars,acc,box,expr) : DirVar =
    (dir,altvar(dirvars,box))

  alt_alt(dirvars,acc,box,expr) : DirVar =
    (even?(length(dirvars)),altvar(dirvars,box))

  interval_minmax(maxdepth,select,le,ge,prune)(expr,box) : Output =
    b_and_b_id(evaluate,branch,subdivide,denorm,combine,prune,le,ge,
               select,accumulate,maxdepth,expr,box)

  VVars(dirvars,box) : nat =
    IF length(box) <= 1 THEN 0
    ELSE mod(length(dirvars),4)
    ENDIF

  VMZ(dirvars,acc,box,expr) : DirVar =
    (True,VVars(dirvars,box))

  sound?(box,expr,M) : bool =
    Proper?(M`mm) IMPLIES
      (FORALL (vs:(vars_in_box?(box))): eval(expr,vs,length(box)) ## M`mm) AND
      Inclusion?(M`lb_box,box) AND
      Inclusion?(M`ub_box,box) AND
      (FORALL (vs:(vars_in_box?(M`lb_box))): eval(expr,vs,length(box)) <= M`lb_max) AND
      (FORALL (vs:(vars_in_box?(M`ub_box))): eval(expr,vs,length(box)) >= M`ub_min)

  interval_minmax_soundness : THEOREM
    sound?(box,expr,interval_minmax(maxdepth,select,le,ge,prune)(expr,box)`ans)

  numerical(maxdepth,precision,select,min_or_max)(expr,box) : Output =
    interval_minmax(maxdepth,select,le_mm(min_or_max,precision),ge_mm,prune_mm(min_or_max))(expr,box)

  numerical_soundness : THEOREM
    sound?(box,expr,numerical(maxdepth,precision,select,min_or_max)(expr,box)`ans)

END numerical_bandb

¤ Dauer der Verarbeitung: 0.20 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

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.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.