The abstract of the Mizar article:

On the Composition of Non-parahalting Macro Instructions

by

Piotr Rudnicki

Received June 3, 1998

MML identifier: SFMASTR1

[ Mizar article, MML identifier index ]

environ

 vocabulary AMI_3, AMI_1, SCMFSA_2, SCMFSA7B, SCMFSA6A, SF_MASTR, SCMFSA6B,
      SCMFSA6C, SCMFSA8C, SCMFSA8B, SCMFSA8A, SCMFSA_4, RELAT_1, AMI_5, BOOLE,
      FUNCT_4, UNIALG_2, FUNCT_1, SCM_1, CARD_1, RELOC, FUNCT_7, FINSET_1,
      SCMFSA_1, SQUARE_1, PRE_FF, ARYTM_1, SFMASTR1;
 notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, NUMBERS, XCMPLX_0,
      XREAL_0, FINSET_1, CARD_1, NAT_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCT_4,
      FUNCT_7, CQC_SIM1, PRE_FF, STRUCT_0, AMI_1, AMI_3, SCM_1, AMI_5,
      SCMFSA_1, SCMFSA_2, SCMFSA_4, SCMFSA_5, SCMFSA6A, SCMFSA6B, SF_MASTR,
      SCMFSA6C, SCMFSA7B, SCMFSA8A, SCMFSA8B, SCMFSA8C;
 constructors NAT_1, SETWISEO, CQC_SIM1, PRE_FF, SCM_1, AMI_5, SCMFSA_1,
      SCMFSA_5, SCMFSA6A, SCMFSA6B, SF_MASTR, SCMFSA6C, SCMFSA8A, SCMFSA8B,
      SCMFSA8C, MEMBERED;
 clusters SUBSET_1, INT_1, FINSET_1, FUNCT_1, AMI_1, SCMFSA_2, SCMFSA_4,
      SF_MASTR, SCMFSA6B, SCMFSA6C, SCMFSA7B, SCMFSA8A, SCMFSA8C, SCMFSA_9,
      RELSET_1, NAT_1, FRAENKEL, MEMBERED, ORDINAL2;
 requirements NUMERALS, SUBSET, BOOLE, ARITHM;


begin :: Good instructions and good macro instructions

definition
 let i be Instruction of SCM+FSA;
 attr i is good means
:: SFMASTR1:def 1

 Macro i is good;
end;

definition
 let a be read-write Int-Location, b be Int-Location;
 cluster a := b -> good;
 cluster AddTo(a, b) -> good;
 cluster SubFrom(a, b) -> good;
 cluster MultBy(a, b) -> good;
end;

definition
 cluster good parahalting Instruction of SCM+FSA;
end;

definition
 let a, b be read-write Int-Location;
 cluster Divide(a, b) -> good;
end;

definition
 let l be Instruction-Location of SCM+FSA;
 cluster goto l -> good;
end;

definition
 let a be Int-Location, l be Instruction-Location of SCM+FSA;
 cluster a =0_goto l -> good;
 cluster a >0_goto l -> good;
end;

definition
 let a be Int-Location, f be FinSeq-Location, b be read-write Int-Location;
 cluster b := (f,a) -> good;
end;

definition
 let f be FinSeq-Location, b be read-write Int-Location;
 cluster b :=len f -> good;
end;

definition
 let f be FinSeq-Location, a be Int-Location;
 cluster f :=<0,...,0> a -> good;
 let b be Int-Location;
 cluster (f,a) := b -> good;
end;

definition
 cluster good Instruction of SCM+FSA;
end;

definition
 let i be good Instruction of SCM+FSA;
 cluster Macro i -> good;
end;

definition
 let i, j be good Instruction of SCM+FSA;
 cluster i ';' j -> good;
end;

definition
 let i be good Instruction of SCM+FSA,
     I be good Macro-Instruction;
 cluster i ';' I -> good;
 cluster I ';' i -> good;
end;

definition
 let a, b be read-write Int-Location;
 cluster swap(a, b) -> good;
end;

definition
 let I be good Macro-Instruction, a be read-write Int-Location;
 cluster Times(a, I) -> good;
end;

theorem :: SFMASTR1:1
 for a being Int-Location, I being Macro-Instruction
  st not a in UsedIntLoc I
   holds I does_not_destroy a;

begin :: Composition of non parahalting macro instructions

 reserve s, S for State of SCM+FSA,
         I, J for Macro-Instruction,
         Ig for good Macro-Instruction,
         i for good parahalting Instruction of SCM+FSA,
         j for parahalting Instruction of SCM+FSA,
         a, b for Int-Location,
         f for FinSeq-Location;
 :: set D = Int-Locations U FinSeq-Locations;

      :: NOTE:
      :: The definition of parahalting seems to be too weak
      :: Why do not we require for parahalting that
      ::           Initialized I is halting

theorem :: SFMASTR1:2
 (I +* Start-At insloc 0) | D = {};

theorem :: SFMASTR1:3
 I is_halting_on Initialize S & I is_closed_on Initialize S &
 J is_closed_on IExec(I, S)
  implies I ';' J is_closed_on Initialize S;

theorem :: SFMASTR1:4
 I is_halting_on Initialize S & J is_halting_on IExec(I, S) &
 I is_closed_on Initialize S & J is_closed_on IExec(I, S)
  implies I ';' J is_halting_on Initialize S;

theorem :: SFMASTR1:5
 I is_closed_on s & I +* Start-At insloc 0 c= s & s is halting
 implies for m being Nat st m <= LifeSpan s
          holds (Computation s).m, (Computation(s+*(I ';' J))).m
                  equal_outside the Instruction-Locations of SCM+FSA;

theorem :: SFMASTR1:6  ::T22
 Ig is_halting_on Initialize s & J is_halting_on IExec(Ig, s) &
 Ig is_closed_on Initialize s & J is_closed_on IExec(Ig, s)
  implies
     LifeSpan (s +* Initialized (Ig ';' J))
         = LifeSpan (s +* Initialized Ig) + 1
         + LifeSpan (Result (s +* Initialized Ig) +* Initialized J);

theorem :: SFMASTR1:7  :: Main theorem
 Ig is_halting_on Initialize s & J is_halting_on IExec(Ig, s) &
 Ig is_closed_on Initialize s & J is_closed_on IExec(Ig, s)
  implies IExec(Ig ';' J, s)
      = IExec(J, IExec(Ig, s))+*Start-At(IC IExec(J, IExec(Ig, s))+card Ig);

theorem :: SFMASTR1:8
 (Ig is parahalting or
              Ig is_halting_on Initialize s & Ig is_closed_on Initialize s) &
 (J is parahalting or
              J is_halting_on IExec(Ig, s) & J is_closed_on IExec(Ig, s))
  implies IExec(Ig ';' J, s).a = IExec(J, IExec(Ig, s)).a;

theorem :: SFMASTR1:9
 (Ig is parahalting or
              Ig is_halting_on Initialize s & Ig is_closed_on Initialize s) &
 (J is parahalting or
              J is_halting_on IExec(Ig, s) & J is_closed_on IExec(Ig, s))
  implies IExec(Ig ';' J, s).f = IExec(J, IExec(Ig, s)).f;

theorem :: SFMASTR1:10
   (Ig is parahalting or
              Ig is_halting_on Initialize s & Ig is_closed_on Initialize s) &
 (J is parahalting or
              J is_halting_on IExec(Ig, s) & J is_closed_on IExec(Ig, s))
  implies IExec(Ig ';' J, s) | D = IExec(J, IExec(Ig, s)) | D;

theorem :: SFMASTR1:11
    Ig is parahalting
 or Ig is_closed_on Initialize s & Ig is_halting_on Initialize s
 implies (Initialize IExec(Ig, s)) | D = IExec(Ig, s) | D;

theorem :: SFMASTR1:12
 Ig is parahalting or
          Ig is_halting_on Initialize s & Ig is_closed_on Initialize s
  implies IExec(Ig ';' j, s).a = Exec(j, IExec(Ig, s)).a;

theorem :: SFMASTR1:13
 Ig is parahalting or
    Ig is_halting_on Initialize s & Ig is_closed_on Initialize s
  implies IExec(Ig ';' j, s).f = Exec(j, IExec(Ig, s)).f;

theorem :: SFMASTR1:14
   Ig is parahalting or
    Ig is_halting_on Initialize s & Ig is_closed_on Initialize s
  implies IExec(Ig ';' j, s) | D = Exec(j, IExec(Ig, s)) | D;

theorem :: SFMASTR1:15
 J is parahalting or
       J is_halting_on Exec(i, Initialize s) &
       J is_closed_on Exec(i, Initialize s)
  implies IExec(i ';' J, s).a = IExec(J, Exec(i, Initialize s)).a;

theorem :: SFMASTR1:16
 J is parahalting or
        J is_halting_on Exec(i, Initialize s) &
        J is_closed_on Exec(i, Initialize s)
  implies IExec(i ';' J, s).f = IExec(J, Exec(i, Initialize s)).f;

theorem :: SFMASTR1:17
   J is parahalting or
       J is_halting_on Exec(i, Initialize s) &
       J is_closed_on Exec(i, Initialize s)
  implies IExec(i ';' J, s) | D = IExec(J, Exec(i, Initialize s)) | D;

begin :: Memory allocation

 reserve L for finite Subset of Int-Locations,
         m, n for Nat;

definition
 let d be Int-Location;
 redefine func { d } -> Subset of Int-Locations;
 let e be Int-Location;
 redefine func { d, e } -> Subset of Int-Locations;
 let f be Int-Location;
 redefine func { d, e, f } -> Subset of Int-Locations;
 let g be Int-Location;
 redefine func { d, e, f, g } -> Subset of Int-Locations;
end;

definition
 let L be finite Subset of Int-Locations;
 func RWNotIn-seq L -> Function of NAT, bool NAT means
:: SFMASTR1:def 2

 it.0 = {k where k is Nat : not intloc k in L & k <> 0} &
 (for i being Nat, sn being non empty Subset of NAT
  st it.i = sn holds it.(i+1) = sn \ {min sn}) &
 for i being Nat holds it.i is infinite;
end;

definition
 let L be finite Subset of Int-Locations, n be Nat;
 cluster (RWNotIn-seq L).n -> non empty;
end;

theorem :: SFMASTR1:18
 not 0 in (RWNotIn-seq L).n &
 (for m st m in (RWNotIn-seq L).n holds not intloc m in L);

theorem :: SFMASTR1:19
 min ((RWNotIn-seq L).n) < min ((RWNotIn-seq L).(n+1));

theorem :: SFMASTR1:20
n < m implies min ((RWNotIn-seq L).n) < min ((RWNotIn-seq L).m);

definition
 let n be Nat, L be finite Subset of Int-Locations;
 func n-thRWNotIn L -> Int-Location equals
:: SFMASTR1:def 3

  intloc min ((RWNotIn-seq L).n);
 synonym n-stRWNotIn L;
 synonym n-ndRWNotIn L;
 synonym n-rdRWNotIn L;
end;

definition
 let n be Nat, L be finite Subset of Int-Locations;
 cluster n-thRWNotIn L -> read-write;
end;

theorem :: SFMASTR1:21
 not n-thRWNotIn L in L;

theorem :: SFMASTR1:22
 n <> m implies n-thRWNotIn L <> m-thRWNotIn L;

definition
 let n be Nat, p be programmed FinPartState of SCM+FSA;
 func n-thNotUsed p -> Int-Location equals
:: SFMASTR1:def 4
             n-thRWNotIn UsedIntLoc p;
 synonym n-stNotUsed p;
 synonym n-ndNotUsed p;
 synonym n-rdNotUsed p;
end;

definition
 let n be Nat, p be programmed FinPartState of SCM+FSA;
 cluster n-thNotUsed p -> read-write;
end;

begin :: A macro for the Fibonacci sequence

theorem :: SFMASTR1:23
 a in UsedIntLoc swap(a, b) & b in UsedIntLoc swap(a, b);

definition
 let N, result be Int-Location;
      ::  set next = 1-stRWNotIn {N, result};
      ::      local variable
      ::  set aux  = 1-stRWNotIn UsedIntLoc swap(result, next);
      ::      for the control variable of Times, must not be changed by swap
      ::  set N_save = 2-ndRWNotIn UsedIntLoc swap(result, next);
      ::      for saving and restoring N

      :: - requires: N <> result
      :: - does not change N
      :: - note: Times allocates no memory

 func Fib_macro (N, result) -> Macro-Instruction equals
:: SFMASTR1:def 5

   N_save := N ';'
   (SubFrom(result, result)) ';'
   (next := intloc 0) ';'
   (aux := N_save) ';'
   Times( aux, AddTo(result, next) ';' swap(result, next) ) ';'
   (N := N_save);
end;

theorem :: SFMASTR1:24
  for N, result being read-write Int-Location
 st N <> result
  for n being Nat st n = s.N
   holds IExec(Fib_macro(N, result), s).result = Fib n &
         IExec(Fib_macro(N, result), s).N = s.N;