Редактирование: ВПнМ/Теормин

Материал из eSyr's wiki.

Перейти к: навигация, поиск

Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.

ПРЕДУПРЕЖДЕНИЕ: Длина этой страницы составляет 87 килобайт. Страницы, размер которых приближается к 32 КБ или превышает это значение, могут неверно отображаться в некоторых браузерах. Пожалуйста, рассмотрите вариант разбиения страницы на меньшие части.

Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.

Текущая версия Ваш текст
Строка 3: Строка 3:
[[Изображение:Verif1.png|400px|thumb|right|Схема верификации на моделях (''Лекция 2, слайд 3'')]]
[[Изображение:Verif1.png|400px|thumb|right|Схема верификации на моделях (''Лекция 2, слайд 3'')]]
-
'''Состояние программы''' - совокупность значений объектов данных и счётчика управления, связанных с некоторой моделью программы.
+
'''Состояние программы''' - совокупность значений переменных и управления, связанных с некоторой моделью программы.
'''Модель''' - упрощённое описание реальности, выполненное с определенной целью.
'''Модель''' - упрощённое описание реальности, выполненное с определенной целью.
Строка 74: Строка 74:
'''Reach(TS)''' - множество всех достижимых состояний в TS
'''Reach(TS)''' - множество всех достижимых состояний в TS
-
'''Трасса''' <math>tr = L(s_0) L(s_1) \dots \in (2^{AP})^\omega</math>; <math>~\omega</math> означает, что трасса может быть бесконечной
+
'''Трасса''' <math>tr = L(s_0) L(s_1) \dots \in (2^{AP})^\omega</math>
====Свойства линейного времени====
====Свойства линейного времени====
Строка 90: Строка 90:
** <math> dom(v) = D_p^v \subseteq D_p</math> -- каждая переменная принадлежит какому-либо домену
** <math> dom(v) = D_p^v \subseteq D_p</math> -- каждая переменная принадлежит какому-либо домену
* <math>n</math> -- подстановка. <math>n: V_p \rightarrow D_p, \forall v \in Var</math> <math>n(v) \in D_p^v</math>
* <math>n</math> -- подстановка. <math>n: V_p \rightarrow D_p, \forall v \in Var</math> <math>n(v) \in D_p^v</math>
-
* <math>~ Cond(V_p)</math> -- Набор булевых условий над <math>V_p</math>
+
* <math>Cond(V_p)</math> -- Набор булевых условий над <math>V_p</math>
-
** формулы пропозициональной логики (<math>p1 \or p2</math>)
+
** формулы пропозициональной логики
-
** условия на переменные вида <math>x \in X</math> (p1: 3<=y<18, p2: f=4)
+
** условия на переменные
-
* <math>~ Eval(Var)</math> -- множество значений переменных. Собственно, это и есть подстановка.
+
* <math>Eval(Var)</math> -- множество значений переменных. Собственно, это и есть подстановка.
* Эффект операторов: <math>Effect: Act \times Eval(Var) \rightarrow Eval(Var)</math>
* Эффект операторов: <math>Effect: Act \times Eval(Var) \rightarrow Eval(Var)</math>
Строка 100: Строка 100:
<math> PG= \langle Loc , Act , Effect ,\rightarrow, Loc_0, g_0 \rangle </math>
<math> PG= \langle Loc , Act , Effect ,\rightarrow, Loc_0, g_0 \rangle </math>
-
* <math>~ Loc</math> -- множество точек
+
* <math>Loc</math> -- множество точек
** <math>Loc_0 \in Loc</math> -- множество начальных точек
** <math>Loc_0 \in Loc</math> -- множество начальных точек
-
* <math>~ Act</math> -- множество действий
+
* <math>Act</math> -- множество действий
* <math>\rightarrow \subseteq Loc \times (Cond(V_p) \times Act) \times Loc </math> -- отношение перехода (<math>Cond(V_p) </math> -- это фактически страж оператора )
* <math>\rightarrow \subseteq Loc \times (Cond(V_p) \times Act) \times Loc </math> -- отношение перехода (<math>Cond(V_p) </math> -- это фактически страж оператора )
-
* <math>~ Effect: Act \times Eval(Var) \rightarrow Eval(Var)</math> -- функция эффекта
+
* <math>Effect</math> -- функция эффекта
* <math>g_0 \in Cond(V_p)</math> -- начальное условие
* <math>g_0 \in Cond(V_p)</math> -- начальное условие
Строка 113: Строка 113:
** находимся в точке программы l
** находимся в точке программы l
** значение переменной x принадлежит некоторому множеству и это множество является подмножеством множеств значений этой переменной.
** значение переменной x принадлежит некоторому множеству и это множество является подмножеством множеств значений этой переменной.
-
* Состояния <math>\langle l,n \rangle</math> размечаются высказыванием о том, что мы находимся в точке программы <math>~ l</math> и всеми высказываниями, истинными в <math>~ n</math>
+
* Состояния <math>\langle l,n \rangle</math> размечаются высказыванием о том, что мы находимся в точке программы l и всеми высказываниями, истинными в n
-
* Если в графе программы есть дуга из <math>~ l</math> в <math>~ l'</math> со стражем <math>~ g</math> и действием <math>~ a</math> и в некоторой подстановке <math>~n</math> выполняется страж <math>~ g</math>, то в системе переходов, которая соответствует этой программе будет присутствовать дуга из состояния <math>\langle l,n\rangle</math> в состояние <math>\langle l', Effect(a,n)\rangle</math> по действию <math>~ a</math>.
+
* Если в графе программы есть дуга из l в <math>l'</math> со стражем g и действием a и в некоторой подстановке n выполняется страж g, то в системе переходов, которая соответствует этой программе будет присутствовать дуга из состояния <math>\langle l,n\rangle</math> в состояние <math>\langle l', Effect(a,n)\rangle</math> по действию a.
'''Системы переходов графов программ'''
'''Системы переходов графов программ'''
Строка 131: Строка 131:
-
'''Пример: Лекция 4, слайд 16'''
+
''Пример: Лекция 4, слайд 16''
-
 
+
-
 
+
-
'''Статическая и операционная семантика'''
+
-
 
+
-
'''Cтатическая семантика''' – набор ограничений, которым должна удовлетворять структура программы;
+
-
'''Операционная семантика''' – понятие состояния программы и изменение состояния в ходе работы программы; то, как по графу строится LTS.
+
-
(См. Л.5, сл. 15, 2010 )
+
=== Параллелизм. Чередование систем переходов. ===
=== Параллелизм. Чередование систем переходов. ===
Строка 216: Строка 209:
Тогда <math>TS_1 \times TS_2 = \langle S_1 \times S_2, Act, \rightarrow, I_1 \times I_2, AP_1 \cup AP_2, L \rangle </math>, где
Тогда <math>TS_1 \times TS_2 = \langle S_1 \times S_2, Act, \rightarrow, I_1 \times I_2, AP_1 \cup AP_2, L \rangle </math>, где
* <math>L(\langle s_1, s_2 \rangle) = L_1(s_1) \cup L_2(s_2)</math>
* <math>L(\langle s_1, s_2 \rangle) = L_1(s_1) \cup L_2(s_2)</math>
-
* <math>\rightarrow</math> определяется как: <math>\frac{s_1 \overset{\alpha}{\rightarrow}_1 s_1' ~ \wedge ~ s_2 \overset{\beta}{\rightarrow}_2 s_2'}{ \langle s_1, s_2 \rangle \overset{\alpha * \beta}{\rightarrow} \langle s_1', s_2' \rangle}</math>
+
* <math>\rightarrow</math> определяется как: <math>\frac{s_1 \overset{\alpha}{\rightarrow}_1 s_1' ~ \wedge ~ s_2 \overset{\beta}{\rightarrow}_2 s_2'}{ \langle s_1, s_2 \rangle \overset{\alpha * \beta}{\rightarrow} \langle s_1', s_2 \rangle}</math>
=== Параллелизм. Асинхронный параллелизм. Системы с каналами. Операционная семантика. ===
=== Параллелизм. Асинхронный параллелизм. Системы с каналами. Операционная семантика. ===
Строка 247: Строка 240:
''Операционная семантика: лекция 4, слайды 44—46''
''Операционная семантика: лекция 4, слайды 44—46''
- 
-
====операционная семантика====
 
- 
-
Пусть <math>CS = \left[PG_1 | PG_2 | \dots | PG_n\right]</math> – система с каналами над <math>(Chan, Var)</math>, и
 
- 
-
<math>PG = \langle Loc, Act, Effect, \rightarrow, Log_0, g_0 \rangle</math>
 
- 
-
Система переходов <math>TS(CS)</math> описывается сигнатурой
 
- 
-
<math>TS(CS) = \langle S, Act, \rightarrow, I , AP, L \rangle </math>, где
 
- 
-
<math>S = ( Loc_1 \times \dots \times Loc_n ) \times Eval(Var) \times Eval(Chan)</math>
 
- 
-
<math>Act = ( \cup_{0 \leqslant i \leqslant n} Act_i ) ~ \cup ~ \tau </math>
 
- 
-
<math>I = \{
 
-
\langle
 
-
l_1, \dots, l_n, \eta, \xi
 
-
\rangle
 
-
|
 
-
\forall i ( l_i \in Loc_{0i} \and \eta \models g_0 ) \and \forall c ( \xi_0(c) = \epsilon )
 
-
\}</math>
 
- 
-
<math>AP = ( \cup_{0 \leqslant i \leqslant n} Loc_i ) \cup Cond(Var)</math>
 
- 
-
<math>L(
 
-
\langle
 
-
l_1, \dots, l_n, \eta, \xi
 
-
\rangle
 
-
) =
 
-
\{
 
-
l_1, \dots, l_n
 
-
\}
 
-
\cup
 
-
\{
 
-
g \in Cond( Var ) | \eta \models g
 
-
\}</math>
 
- 
-
'''Правила вывода'''
 
-
<ul>
 
-
<li> <p> интерливинг для <math> \alpha \in Act_i </math> </p>
 
-
<p><math>
 
-
\frac
 
-
{l_i \overset{g:\alpha}{\rightarrow} l_i' \and n \models g }
 
-
{
 
-
\langle
 
-
l_1, \dots , l_i, \dots , l_n , \eta, \xi
 
-
\rangle
 
-
\overset{\alpha}{\rightarrow}
 
-
\langle
 
-
l_1, \dots, l_i', \dots, l_n , \eta', \xi
 
-
\rangle
 
-
}
 
-
</math></p>
 
- 
-
</li>
 
-
<li> <p>Синхронная передача сообщений через <math>c \in Chan, cap(c) = 0</math></p>
 
- 
-
<p>
 
-
<math>
 
-
\frac
 
-
{
 
-
l_i \overset{c?x}{\rightarrow} l_i' \and
 
-
l_j \overset{c!v}{\rightarrow} l_j' \and
 
-
i \neq j
 
-
}
 
-
{
 
-
\langle
 
-
l_1, \dots , l_i, \dots, l_j, \dots , l_n , \eta, \xi
 
-
\rangle
 
-
\overset{\alpha}{\rightarrow}
 
-
\langle
 
-
l_1, \dots, l_i', \dots, l_j', \dots , l_n , \eta', \xi
 
-
\rangle
 
-
}
 
-
</math>
 
-
</p>
 
-
</li>
 
-
<li>
 
-
<p>
 
-
Асинхронная передача сообщений через <math>c \in Chan, cap(c) \neq 0</math>
 
-
</p>
 
-
<ul>
 
-
<li>
 
-
<p>
 
-
получить значение по каналу c и присвоить переменной x:
 
-
</p>
 
- 
-
<p>
 
-
<math>
 
-
\frac
 
-
{
 
-
l_i \overset{c?x}{\rightarrow} l_i' \and
 
-
len(\xi(c))=k>0) \and
 
-
\xi(c)=v_1 \dots vk
 
-
}
 
-
{
 
-
\langle
 
-
l_1, \dots , l_i, \dots , l_n , \eta, \xi
 
-
\rangle
 
-
\overset{c?x}{\rightarrow}
 
-
\langle
 
-
l_1, \dots, l_i', \dots, l_n , \eta', \xi'
 
-
\rangle
 
-
}
 
-
</math>,
 
-
</p>
 
- 
-
<p>
 
-
где
 
-
<math>
 
-
\eta' = \eta[x=v_1], \xi'=\xi[c=v_2 \dots v_k ]
 
-
</math>
 
-
</p>
 
- 
-
</li>
 
- 
-
<li>
 
-
<p>
 
-
передать значение <math>v \in dom(c) </math> по каналу c:
 
-
</p>
 
-
<p>
 
-
<math>
 
-
\frac
 
-
{
 
-
l_i \overset{c!v}{\rightarrow} l_i' \and
 
-
len(\xi(c))=k<cap(c)) \and
 
-
\xi(c)=v_1 \dots vk
 
-
}
 
-
{
 
-
\langle
 
-
l_1, \dots , l_i, \dots , l_n , \eta, \xi
 
-
\rangle
 
-
\overset{c!v}{\rightarrow}
 
-
\langle
 
-
l_1, \dots, l_i', \dots, l_n , \eta, \xi'
 
-
\rangle
 
-
}
 
-
</math>,
 
-
</p>
 
-
<p>
 
-
где
 
-
<math>
 
-
\xi'=\xi[c=v_1 \dots v_k v ]
 
-
</math>
 
-
</p>
 
-
</li>
 
-
</ul>
 
-
</li>
 
-
</ul>
 
- 
-
<math></math>
 
-
<math></math>
 
=== Абстракция. Абстракция трасс. Абстракция системы переходов. Необходимое и достаточное условие корректности LTS модели. ===
=== Абстракция. Абстракция трасс. Абстракция системы переходов. Необходимое и достаточное условие корректности LTS модели. ===
Строка 412: Строка 252:
* <math>I(tr') = \langle\mathbb{N}, \leqslant, \xi'\rangle, ~~ \xi: \mathbb{N} \times AP' = \{true, false\}</math>
* <math>I(tr') = \langle\mathbb{N}, \leqslant, \xi'\rangle, ~~ \xi: \mathbb{N} \times AP' = \{true, false\}</math>
-
Будем говорить, что трасса tr' является '''абстракцией трассы''' tr (<math>tr \prec tr'</math>), если
+
Будем говорить, что трасса tr' является '''абстракцией трассы''' tr (<math>tr \leqslant tr'</math>), если
# <math>AP' \subseteq AP</math>
# <math>AP' \subseteq AP</math>
# <math>\exists \alpha : \mathbb{N} \rightarrow \mathbb{N}</math> такое, что
# <math>\exists \alpha : \mathbb{N} \rightarrow \mathbb{N}</math> такое, что
Строка 420: Строка 260:
Пример абстракции трассы: Лекция 2, слайд 53
Пример абстракции трассы: Лекция 2, слайд 53
-
'''Определение.''' Пусть P – система, φ – произвольное свойство линейного времени. '''Корректной моделью ''' P называется такая М, что:
+
''' Необходимое условие корректности модели ''' - <math>\forall tr \in Traces(TS(P)) ~ \exists tr' \in Traces(TS(M)) ~ : ~ tr \leqslant tr'</math>, где
-
<math> M \models \phi \Rightarrow P \models \phi </math>.
+
* <math>P</math> - система
-
''(позволяет проверять свойства программы на её модели )''
+
* <math>M</math> - модель этой системы
-
''' Необходимое и достаточное условие корректности модели:'''
+
При этом, если <math>\varphi</math> - некоторое свойство системы, то <math>M \models \varphi ~ \Rightarrow ~ P \models \varphi</math> выполняется тогда и только тогда, когда верно условие корректности модели.
-
Модель <math>M</math> системы <math>P</math> корректна тогда и только тогда, когда <math>\forall tr \in Traces(TS(P)) ~ \exists tr' \in Traces(TS(M)) ~ : ~ tr \prec tr'</math>.
+
-
''(для проверки такого условия нужно рассмотреть все трассы исходной системы, допускает, что в модели
+
-
больше состояний )''
+
=== Абстракция. Абстракция системы переходов. Достаточное условие корректности LTS модели. Адекватность LTS модели. ===
=== Абстракция. Абстракция системы переходов. Достаточное условие корректности LTS модели. Адекватность LTS модели. ===
Строка 444: Строка 281:
** Каждому переходу из системы должен соответствовать переход в модели: <math>s^1_1 \rightarrow_1 s^1_2 ~ \Rightarrow ~ a(s^1_1) \rightarrow_2 a(s^1_2)</math>
** Каждому переходу из системы должен соответствовать переход в модели: <math>s^1_1 \rightarrow_1 s^1_2 ~ \Rightarrow ~ a(s^1_1) \rightarrow_2 a(s^1_2)</math>
* Метки на состояниях модели должны состоять только из предикатов модели: <math>\forall s \in S^1: L^2(a(s)) = L^1(s) \cap 2^{AP^2}</math>
* Метки на состояниях модели должны состоять только из предикатов модели: <math>\forall s \in S^1: L^2(a(s)) = L^1(s) \cap 2^{AP^2}</math>
- 
-
Модель называется '''адекватной''', если:
 
-
* Атомарные высказывания, в терминах которых задаются свойства, присутствуют в разметке модели. ''(Необходимое условие)''
 
-
* Из нарушения свойства на модели следует, что оно нарушается и на исходной системе. ''(Достаточное условие)''
 
'''Необходимое условие адекватности модели свойствам правильности''': алфавит предикатов свойств правильности включен в алфавит предикатов модели — <math>AP_\phi \subseteq AP_M</math>. Условие не является достаточным (см. примеры, лекция 3, слайды 4—5).
'''Необходимое условие адекватности модели свойствам правильности''': алфавит предикатов свойств правильности включен в алфавит предикатов модели — <math>AP_\phi \subseteq AP_M</math>. Условие не является достаточным (см. примеры, лекция 3, слайды 4—5).
Строка 575: Строка 408:
** <math>U</math> (U) — до тех пор, пока (until)
** <math>U</math> (U) — до тех пор, пока (until)
-
====Выполнимость формул:====
+
'''Сильный Until:'''
-
* Задаётся последовательность состояний прохода <math>\sigma: s_0, s_1, s_2, \dots</math>
+
* всегда e, до тех пор, пока не f, при этом f обязательно должно наступить
-
* <math>\forall i, i \geqslant 0, ~ \forall p </math> определена выполнимость <math> p </math> в <math> s_i </math>
+
* <math>s_i \models e U f ~~ \Leftrightarrow ~~ \begin{cases}
-
* Семантика LTL:
+
-
** <math>\sigma \models f \Leftrightarrow s_0 \models f</math>
+
-
** <math>s_i \models \Box f \Leftrightarrow \forall j, j \geqslant i: s_j \models f</math>
+
-
** <math>s_i \models \Diamond f \Leftrightarrow \exists j, j \geqslant i: s_j \models f</math>
+
-
** <math>s_i \models Xf \Leftrightarrow s_{i+1} \models f </math>
+
-
** '''Слабый Until:'''
+
-
*** всегда e, до тех пор, пока не f, при этом не факт, что f наступает (тогда всегда e)
+
-
*** <math>s_i \models e W f ~~ \Leftrightarrow ~~ s_i \models f \vee (s_i \models e \wedge s_{i+1} \models e W f)</math>
+
-
** '''Сильный Until:'''
+
-
*** всегда e, до тех пор, пока не f, при этом f обязательно должно наступить
+
-
*** <math>s_i \models e U f ~~ \Leftrightarrow ~~ \begin{cases}
+
\exists j, j \geqslant i: ~ s_j \models f \\
\exists j, j \geqslant i: ~ s_j \models f \\
\forall k, i \leqslant k < j: ~ s_k \models e
\forall k, i \leqslant k < j: ~ s_k \models e
\end{cases}</math>
\end{cases}</math>
 +
 +
'''Слабый Until:'''
 +
* всегда e, до тех пор, пока не f, при этом не факт, что f наступает (тогда всегда e)
 +
* <math>s_i \models e \cup f ~~ \Leftrightarrow ~~ s_i \models f \vee (s_i \models e \wedge s_{i+1} \models e \cup f)</math>
 +
 +
<u>Выполнимость формул:</u>
 +
* Задаётся последовательность состояний прохода <math>\sigma</math>
 +
* <math>\forall i, i \geqslant 0, ~ \forall p ~~ : ~~ s_i \models p </math> ('''Внимание'''!! ''это слишком смахивает на бред, который должен быть интуитивно понятен. Если кто может - распишите подробнее выполнимость!!'' может быть, здесь имеется в виду что в каждом состоянии определена формула, или что если есть формула, то она определена в каком-то состоянии. вообщем, wierd).
=== Логика LTL. Основные типы свойств LTL. Цикличность, стабильность, инвариант, гарантия, отклик, приоритет, корреляция. ===
=== Логика LTL. Основные типы свойств LTL. Цикличность, стабильность, инвариант, гарантия, отклик, приоритет, корреляция. ===
Строка 884: Строка 714:
* Кларк, Эмерсон, 1981 и Квили, Сифакис, 1982 – model checking (обход достижимых состояний),
* Кларк, Эмерсон, 1981 и Квили, Сифакис, 1982 – model checking (обход достижимых состояний),
* Варди и Вольпер, 1986 – новая техника model checking (анализ конформности),
* Варди и Вольпер, 1986 – новая техника model checking (анализ конформности),
-
* Хольцман, 1989 – верификатор SPIN.
+
* Хольцман, 1981 – верификатор SPIN.
* Бриан, 1989 – Двоичные решающие диаграммы (BDD),
* Бриан, 1989 – Двоичные решающие диаграммы (BDD),
* МакМиллан, 1993 – верификатор SMV (символьная верификация, BDD),
* МакМиллан, 1993 – верификатор SMV (символьная верификация, BDD),
Строка 901: Строка 731:
'' Лекция 2, Слайды 3-4 ''
'' Лекция 2, Слайды 3-4 ''
-
====Примеры классов свойств:====
+
<u>Примеры классов свойств:</u>
* Стандартные
* Стандартные
-
** Отсутствие ошибок времени выполнения (RTE),
 
-
** Отсутствие удушения (starvation),
 
-
** Не срабатывают ассерты(assertions).
 
** [http://en.wikipedia.org/wiki/Deadlock deadlocks] ([http://ru.wikipedia.org/wiki/%D0%92%D0%B7%D0%B0%D0%B8%D0%BC%D0%BD%D0%B0%D1%8F_%D0%B1%D0%BB%D0%BE%D0%BA%D0%B8%D1%80%D0%BE%D0%B2%D0%BA%D0%B0 взаимная блокировка])
** [http://en.wikipedia.org/wiki/Deadlock deadlocks] ([http://ru.wikipedia.org/wiki/%D0%92%D0%B7%D0%B0%D0%B8%D0%BC%D0%BD%D0%B0%D1%8F_%D0%B1%D0%BB%D0%BE%D0%BA%D0%B8%D1%80%D0%BE%D0%B2%D0%BA%D0%B0 взаимная блокировка])
** [http://en.wikipedia.org/wiki/Race_condition Race condition] ([http://ru.wikipedia.org/wiki/%D0%A1%D0%BE%D1%81%D1%82%D0%BE%D1%8F%D0%BD%D0%B8%D0%B5_%D0%B3%D0%BE%D0%BD%D0%BA%D0%B8 состояние гонки])
** [http://en.wikipedia.org/wiki/Race_condition Race condition] ([http://ru.wikipedia.org/wiki/%D0%A1%D0%BE%D1%81%D1%82%D0%BE%D1%8F%D0%BD%D0%B8%D0%B5_%D0%B3%D0%BE%D0%BD%D0%BA%D0%B8 состояние гонки])
Строка 912: Строка 739:
** корректная завершаемость
** корректная завершаемость
** причинно-следственный и темпоральный порядок состояний системы
** причинно-следственный и темпоральный порядок состояний системы
-
** Инварианты системы,
 
-
** Индикаторы прогресса,
 
- 
-
====Схема верификации на модели====
 
-
[[Изображение:Verif1.png|400px|Схема верификации на моделях (''Лекция 2, слайд 3'')]]
+
''Схема верификации на модели: Лекция 2, слайд 3''
=== Верификация при помощи Spin. Задание свойств состояний. ===
=== Верификация при помощи Spin. Задание свойств состояний. ===

Пожалуйста, обратите внимание, что все ваши добавления могут быть отредактированы или удалены другими участниками. Если вы не хотите, чтобы кто-либо изменял ваши тексты, не помещайте их сюда.
Вы также подтверждаете, что являетесь автором вносимых дополнений, или скопировали их из источника, допускающего свободное распространение и изменение своего содержимого (см. eSyr's_wiki:Авторское право).
НЕ РАЗМЕЩАЙТЕ БЕЗ РАЗРЕШЕНИЯ ОХРАНЯЕМЫЕ АВТОРСКИМ ПРАВОМ МАТЕРИАЛЫ!

Шаблоны, использованные на этой странице:

Личные инструменты
Разделы