Bezpieczna dealokacja obiektów - Historia wersji

AndrzejSalwicki: /* Bibliografia */

2015-10-22T19:39:02Z

‎Bibliografia

AndrzejSalwicki: /* Bibliografia */

2015-10-22T19:37:50Z

‎Bibliografia

AndrzejSalwicki: /* Bibliografia */

2015-10-22T19:30:21Z

‎Bibliografia

AndrzejSalwicki: /* Bibliografia */

2015-10-22T19:25:49Z

‎Bibliografia

AndrzejSalwicki: /* Zobacz też */

2015-01-18T18:17:55Z

‎Zobacz też

AndrzejSalwicki: /* Acknowledgement */

2015-01-18T18:14:51Z

‎Acknowledgement

AndrzejSalwicki: /* Algorithmic specification ATHM of heap management */

2015-01-17T19:42:14Z

‎Algorithmic specification ATHM of heap management

AndrzejSalwicki: /* Algorithmic specification ATHM of heap management */

2015-01-17T19:40:37Z

‎Algorithmic specification ATHM of heap management

AndrzejSalwicki: /* Algorithmic specification ATHM of heap management */

2015-01-17T19:37:38Z

‎Algorithmic specification ATHM of heap management

AndrzejSalwicki: /* Algorithmic specification ATHM of heap management */

2015-01-17T19:31:58Z

‎Algorithmic specification ATHM of heap management

← poprzednia wersja		Wersja z 19:39, 22 paź 2015
Linia 314:		Linia 314:

	# [Kreczmar, Cioni 1984] [[ Media:Programmed-deallocation-without-Dangling-Reference-I.pdf\|{{Cytuj pismo\| odn=tak \| imię=Antoni \| nazwisko=Kreczmar\| imię2=Gianna \| nazwisko2=Cioni \|tytuł=Programmed deallocation without dangling reference \|czasopismo=Information Processing Letters \|strony=179-187 \|rok=1984}}]]		# [Kreczmar, Cioni 1984] [[ Media:Programmed-deallocation-without-Dangling-Reference-I.pdf\|{{Cytuj pismo\| odn=tak \| imię=Antoni \| nazwisko=Kreczmar\| imię2=Gianna \| nazwisko2=Cioni \|tytuł=Programmed deallocation without dangling reference \|czasopismo=Information Processing Letters \|strony=179-187 \|rok=1984}}]]
−	~~http://lem12.uksw.edu.pl/wiki/Plik:Programmed-deallocation-without-Dangling-Reference-I.pdf~~

← poprzednia wersja		Wersja z 19:37, 22 paź 2015
Linia 313:		Linia 313:
	== Bibliografia ==		== Bibliografia ==

−	# [Kreczmar, Cioni 1984] [[ Media:Programmed-~~dealocation~~-without-~~dangling~~-~~reference~~-I.pdf\|{{Cytuj pismo\| odn=tak \| imię=Antoni \| nazwisko=Kreczmar\| imię2=Gianna \| nazwisko2=Cioni \|tytuł=Programmed deallocation without dangling reference \|czasopismo=Information Processing Letters \|strony=179-187 \|rok=1984}}]]	+	# [Kreczmar, Cioni 1984] [[ Media:Programmed-deallocation-without-Dangling-Reference-I.pdf\|{{Cytuj pismo\| odn=tak \| imię=Antoni \| nazwisko=Kreczmar\| imię2=Gianna \| nazwisko2=Cioni \|tytuł=Programmed deallocation without dangling reference \|czasopismo=Information Processing Letters \|strony=179-187 \|rok=1984}}]]
		+	http://lem12.uksw.edu.pl/wiki/Plik:Programmed-deallocation-without-Dangling-Reference-I.pdf

← poprzednia wersja		Wersja z 19:30, 22 paź 2015
Linia 313:		Linia 313:
	== Bibliografia ==		== Bibliografia ==

−	# [Kreczmar, Cioni 1984] [[ Media:Programmed-dealocation-without-dangling-reference-I.pdf\|{{Cytuj pismo\| odn=tak \| imię=Antoni \| nazwisko=Kreczmar\| imię2=Gianna \| nazwisko2=Cioni \|tytuł=Programmed deallocation without dangling reference \|czasopismo=Information Processing Letters \|strony=179-187 \|rok=1984~~\|url=http://lem12.uksw.edu.pl/wiki/Programmed_dealocation_without_dangling_reference.pdf~~}}]]	+	# [Kreczmar, Cioni 1984] [[ Media:Programmed-dealocation-without-dangling-reference-I.pdf\|{{Cytuj pismo\| odn=tak \| imię=Antoni \| nazwisko=Kreczmar\| imię2=Gianna \| nazwisko2=Cioni \|tytuł=Programmed deallocation without dangling reference \|czasopismo=Information Processing Letters \|strony=179-187 \|rok=1984}}]]

← poprzednia wersja		Wersja z 19:25, 22 paź 2015
Linia 313:		Linia 313:
	== Bibliografia ==		== Bibliografia ==

−	# [Kreczmar, Cioni 1984] [[Media:Programmed-dealocation-without-dangling-reference-I.pdf\|{{Cytuj pismo\| odn=tak \| imię=Antoni \| nazwisko=Kreczmar\| imię2=Gianna \| nazwisko2=Cioni \|tytuł=Programmed deallocation without dangling reference \|czasopismo=Information Processing Letters \|strony=179-187 \|rok=1984\|url=http://lem12.uksw.edu.pl/wiki/Programmed_dealocation_without_dangling_reference}}]]	+	# [Kreczmar, Cioni 1984] [[ Media:Programmed-dealocation-without-dangling-reference-I.pdf\|{{Cytuj pismo\| odn=tak \| imię=Antoni \| nazwisko=Kreczmar\| imię2=Gianna \| nazwisko2=Cioni \|tytuł=Programmed deallocation without dangling reference \|czasopismo=Information Processing Letters \|strony=179-187 \|rok=1984\|url=http://lem12.uksw.edu.pl/wiki/Programmed_dealocation_without_dangling_reference.pdf}}]]

← poprzednia wersja		Wersja z 18:17, 18 sty 2015
Linia 311:		Linia 311:
	{{Przypisy}}		{{Przypisy}}
	<references/>		<references/>
		+	== Bibliografia ==
		+
		+	# [Kreczmar, Cioni 1984] [[Media:Programmed-dealocation-without-dangling-reference-I.pdf\|{{Cytuj pismo\| odn=tak \| imię=Antoni \| nazwisko=Kreczmar\| imię2=Gianna \| nazwisko2=Cioni \|tytuł=Programmed deallocation without dangling reference \|czasopismo=Information Processing Letters \|strony=179-187 \|rok=1984\|url=http://lem12.uksw.edu.pl/wiki/Programmed_dealocation_without_dangling_reference}}]]

← poprzednia wersja		Wersja z 18:14, 18 sty 2015
Linia 305:		Linia 305:

	The second author was financed by research fellowship within the Project ''Information technologies: Research and its interdisciplinary applications'', Agreement number UDA POKL.04.01.01-00-051/10-00.		The second author was financed by research fellowship within the Project ''Information technologies: Research and its interdisciplinary applications'', Agreement number UDA POKL.04.01.01-00-051/10-00.
		+	== Zobacz też ==
		+	* [[odśmiecanie pamięci]]

−	<references />	+	{{Uwagi}}
		+	{{Przypisy}}
		+	<references/>

@@ Linia 228: / Linia 228: @@
 HM$_6$) $\forall_{f \in F}\forall_{s \in S}\{s':=del(f,s) \}(\lnot mb(f,s')\wedge \forall_{f' \in F}(f'\neq f \implies mb(f',s)\Leftrightarrow    mb(f',s'))$ <br />
 <small> operation $del$ deletes frame $f$ from the state $s $  </small> <br />
-HM$_7$)] $mb(f,s)  \Leftrightarrow
+HM$_7$) $mb(f,s)  \Leftrightarrow
    \left \{ \begin{array}{l}
      \mbox{begin} \\
@@ Linia 242: / Linia 242: @@
    \right \} bool $  <br />
 <small> This formula defines the properties of relation member.  It is '''not''' an implementation.  We postulate  that the implemented cost should be constant. </small> <br />
-HM$_8$)] <small> The operation kill is characterised by the axioms of the following scheme.   The index $k$ may be any natural number $k>0$, let $1 \leq i \leq k$. </small> <br />
+HM$_8$) <small> The operation kill is characterised by the axioms of the following scheme.   The index $k$ may be any natural number $k>0$, let $1 \leq i \leq k$. </small> <br />
 $\underbrace{((f_1=   ... =f_k) \wedge mb(f_1,s))}_{precondition}\Rightarrow \underbrace{[s' :=kill(f_i,s)]}_{\mathrm{statement}}\underbrace{(f_1=   ... =f_k   = \textbf{none})}_{postcondition}  $  <br />
 <small>  Any formula of this form is an axiom, it tells that operation kill in one move nullifies ''all the references to the object pointed by the variable'' $f_i$.  And indeed,  in the system of Kreczmar the cost of the operation kill is constant.   </small> <br />

@@ Linia 210: / Linia 210: @@
 HM$_1$) $\forall_{s \in S}\ \neg \,mb(res(s),s)$ <br />
-<small><small> For every state $s$, operation $res(s)$ returns a new frame, not an element of $s$ </small></small> <br />
+<small> For every state $s$, operation $res(s)$ returns a new frame, not an element of $s$ </small> <br />
 HM$_2$) $\forall_{f \in F}\ \lnot \, mb(f, eS)$  <br />
-<small><small> the initstate $eS$ is the empty set of frames </small></small><br />
+<small> the initstate $eS$ is the empty set of frames </small><br />
 HM$_3$)  $\forall_{s \in S}\,
   \left \{ \begin{array}{l}
@@ Linia 221: / Linia 221: @@
   \end{array} \right \}\, (s = eS)$ <br />
-<small><small> For every state $s$, the program while (above) terminates, hence, every state is a finite set of frames</small></small> <br />
+<small> For every state $s$, the program while (above) terminates, hence, every state is a finite set of frames </small> <br />
 HM$_4$) $\forall_{s \in S} \ s\neq eS \Rightarrow mb(amb(s),s)$ <br />
-<small><small> For every non-empty state, function $amb$ returns a member of the state $s$ </small></small> <br />
+<small> For every non-empty state, function $amb$ returns a member of the state $s$ </small> <br />
 HM$_5$) $\forall_{f \in F}\forall_{s \in S}\{s':=ins(f,s)\}(mb(f,s')\wedge \forall_{f' \in F}(f'\neq f \implies mb(f',s) \Leftrightarrow mb(f',s')) $<br />
-<small><small> operation $ins$ adds frame $f$ to the state $s$ </small></small> <br />
+<small> operation $ins$ adds frame $f$ to the state $s$ </small> <br />
 HM$_6$) $\forall_{f \in F}\forall_{s \in S}\{s':=del(f,s) \}(\lnot mb(f,s')\wedge \forall_{f' \in F}(f'\neq f \implies mb(f',s)\Leftrightarrow    mb(f',s'))$ <br />
-<small><small> operation $del$ deletes frame $f$ from the state $s $  </small></small> <br />
+<small> operation $del$ deletes frame $f$ from the state $s $  </small> <br />
 HM$_7$)] $mb(f,s)  \Leftrightarrow
    \left \{ \begin{array}{l}
@@ Linia 242: / Linia 242: @@
    \right \} bool $  <br />
 <small> This formula defines the properties of relation member.  It is '''not''' an implementation.  We postulate  that the implemented cost should be constant. </small> <br />
-HM$_8$)] <small><small> The operation kill is characterised by the axioms of the following scheme.   The index $k$ may be any natural number $k>0$, let $1 \leq i \leq k$. </small></small> <br />
+HM$_8$)] <small> The operation kill is characterised by the axioms of the following scheme.   The index $k$ may be any natural number $k>0$, let $1 \leq i \leq k$. </small> <br />
 $\underbrace{((f_1=   ... =f_k) \wedge mb(f_1,s))}_{precondition}\Rightarrow \underbrace{[s' :=kill(f_i,s)]}_{\mathrm{statement}}\underbrace{(f_1=   ... =f_k   = \textbf{none})}_{postcondition}  $  <br />
-<small><small>  Any formula of this form is an axiom, it tells that operation kill in one move nullifies ''all the references to the object pointed by the variable'' $f_i$.  And indeed,  in the system of Kreczmar the cost of the operation kill is constant.   </small></small> <br />
+<small>  Any formula of this form is an axiom, it tells that operation kill in one move nullifies ''all the references to the object pointed by the variable'' $f_i$.  And indeed,  in the system of Kreczmar the cost of the operation kill is constant.   </small> <br />
 == Properties of the specification ==

@@ Linia 224: / Linia 224: @@
 HM$_4$) $\forall_{s \in S} \ s\neq eS \Rightarrow mb(amb(s),s)$ <br />
 <small><small> For every non-empty state, function $amb$ returns a member of the state $s$ </small></small> <br />
-HM$_5$) $\forall_{f \in F}\forall_{s \in S}\{s':=ins(f,s)\}(mb(f,s')\wedge \forall_{f' \in F}(f'\neq f \implies mb(f',s) \Leftrightarrow mb(f',s')) $
+HM$_5$) $\forall_{f \in F}\forall_{s \in S}\{s':=ins(f,s)\}(mb(f,s')\wedge \forall_{f' \in F}(f'\neq f \implies mb(f',s) \Leftrightarrow mb(f',s')) $<br />
 <small><small> operation $ins$ adds frame $f$ to the state $s$ </small></small> <br />
 HM$_6$) $\forall_{f \in F}\forall_{s \in S}\{s':=del(f,s) \}(\lnot mb(f,s')\wedge \forall_{f' \in F}(f'\neq f \implies mb(f',s)\Leftrightarrow    mb(f',s'))$ <br />
@@ Linia 230: / Linia 230: @@
 HM$_7$)] $mb(f,s)  \Leftrightarrow
    \left \{ \begin{array}{l}
-     '''begin''' \\
+     \mbox{begin} \\
      \quad s1 := s;\ bool := false; \\
-     \quad '''while''' \ s1 \neq eS \wedge \lnot bool \\
+     \quad \mbox{while} \ s1 \neq eS \wedge \lnot bool \\
-     \quad '''do''' \\
+     \quad \mbox{do} \\
      \qquad f1 := amb(s1); \\
-     \qquad '''if''' \ f=f1 \ '''then''' \ bool := true \ '''fi'''; \\
+     \qquad \mbox{if} \ f=f1 \ \mbox{then} \ bool := true \ \mbox{fi}; \\
      \qquad s1 :=del(f1,s1); \\
-     \quad '''od''' \\
+     \quad \mbox{od} \\
-     '''end''' \
+     \mbox{end} \
    \end{array}
    \right \} bool $  <br />
-<small><small> This formula defines the properties of relation member.  It is '''not''' an implementation.  We postulate  that the implemented cost should be constant. </small></small> <br />
+<small> This formula defines the properties of relation member.  It is '''not''' an implementation.  We postulate  that the implemented cost should be constant. </small> <br />
 HM$_8$)] <small><small> The operation kill is characterised by the axioms of the following scheme.   The index $k$ may be any natural number $k>0$, let $1 \leq i \leq k$. </small></small> <br />
 $\underbrace{((f_1=   ... =f_k) \wedge mb(f_1,s))}_{precondition}\Rightarrow \underbrace{[s' :=kill(f_i,s)]}_{\mathrm{statement}}\underbrace{(f_1=   ... =f_k   = \textbf{none})}_{postcondition}  $  <br />