LectLog22 (Старые лекции, в целом тоже самое), страница 2

PDF-файл LectLog22 (Старые лекции, в целом тоже самое), страница 2 Математическая логика и логическое программирование (53130): Лекции - 7 семестрLectLog22 (Старые лекции, в целом тоже самое) - PDF, страница 2 (53130) - СтудИзба2019-09-18СтудИзба

Описание файла

Файл "LectLog22" внутри архива находится в папке "Старые лекции, в целом тоже самое". PDF-файл из архива "Старые лекции, в целом тоже самое", который расположен в категории "". Всё это находится в предмете "математическая логика и логическое программирование" из 7 семестр, которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .

Просмотр PDF-файла онлайн

Текст 2 страницы из PDF

, χ0k Uχ00k , χ0k+1 Rχ00k+1 , . . . , χ0k+m Rχ00k+m }.Каждой формуле ψi из множества URSubϕ1 сопоставиминдивидуальный цвет i.Раскрасим в цвет i все вершины (s, B), для которых выполненохотя бы одно из двух условийв случае, когда ψi = χ0i Uχ00i :1) χ00i ∈ B,2) X(χ0i Uχ00i ) ∈/ B.в случае, когда ψi = χ0i Rχ00i :/ B,1) χ00i ∈2) X(χ0i Rχ00i ) ∈ B.Бесконечный маршрут(si1 , Bi1 ), (si2 , Bi2 ), . . .

, (sin , Bin ), . . .в графе Γϕ1 ,M назовем радужным, если в нем бесконечно частовстречаются вершины каждого цвета 1, 2, . . . , k.ТАБЛИЧНЫЙ МЕТОД ВЕРИФИКАЦИИОсновная теоремаДля любой формулы PLTL ϕ1 в позитивной форме и LTSM = hAP, S, S0 , −→, ρiM 6|= ϕ1mв графе Γϕ1 ,M существует хотя бы один радужный маршрут,исходящий из вершины v0 = (s0 , B0 ), в которой s0 ∈ S0 иϕ1 ∈/ B0 .ТАБЛИЧНЫЙ МЕТОД ВЕРИФИКАЦИИДоказательство.(⇑) Предположим, что в графе Γϕ1 ,M есть радужный маршрут(s0 , B0 ), (s1 , B1 ), . .

. , (sn , Bn ), (sn+1 , Bn+1 ), . . .указанного вида, в котором ϕ1 ∈/ B0 .Тогда согласно определению системы Хинтикки Γϕ1 ,M в LTS Mесть начальная трассаtr |0 |= B0tr = ys0tr |1 |= B1tr |2 |= B2- y- ys1s2- r r rtr |n |= Bn- ysntr |n+1 |= Bn+1- y- r r rsn+1Покажем, что для любой формулы ψ, ψ ∈ FLSubϕ1 , и длялюбого n, n ≥ 0, верноtr |n |= ψ ⇐⇒ ψ ∈ Bn .ТАБЛИЧНЫЙ МЕТОД ВЕРИФИКАЦИИДоказательство.Если удастся показать, чтоtr |n |= ψ ⇐⇒ ψ ∈ Bn(∗)то, учитывая ϕ1 ∈/ B0 , придем к заключению tr 6|= ϕ1 .Для доказательства соотношения (∗) воспользуемся индукциейпо числу связок в формуле ψ.Базис индукции.

p ∈ AP.p ∈ Bn ⇐⇒ p ∈ ξ(sn ) ⇐⇒ tr |n |= p .¬p ∈ Bn ⇐⇒ p ∈/ Bn ⇐⇒ p ∈/ ξ(sn ) ⇐⇒ tr |n 6|= p ⇐⇒ tr |n |= ¬p.ТАБЛИЧНЫЙ МЕТОД ВЕРИФИКАЦИИДоказательство.Индуктивный переход.1. Логические связки & и ∨.ψ1 &ψ2 ∈ Bn ⇐⇒ ψ1 ∈ Bn и ψ2 ∈ Bn ⇐⇒ tr |n |= ψ1 и tr |n |= ψ1⇐⇒ tr |n |= ψ1 &ψ1 .2.

Темпоральный оператор X.Xψ ∈ Bn ⇐⇒ ψ ∈ Bn+1 ⇐⇒ tr |n+1 |= ψ ∈ Bn+1 ⇐⇒ tr |n |= Xψ.ТАБЛИЧНЫЙ МЕТОД ВЕРИФИКАЦИИИндуктивный переход.3. Темпоральный оператор R.3.1. Покажем ψ1 Rψ2 ∈ Bn =⇒ tr |n |= ψ1 Rψ2 .Заметим, что согласно определению согласованного множестваψ1 Rψ2 ∈ B ⇐⇒ ψ2 ∈ B и при этом ψ1 ∈ B или X(ψ1 Rψ2 ) ∈ B.Пусть ψ1 Rψ2 ∈ Bn . Тогда возможны 2 случая.Вариант 1. X(ψ1 Rψ2 ) ∈ Bn+i для любого i, i ≥ 0.Тогда по определению Γϕ1 ,M в каждом множестве Bn+i , i ≥ 0,содержится формула ψ1 Rψ2 и, следовательно, ψ2 ∈ Bn+i .Тогда по индуктивному предположению tr |n+i |= ψ2 для любогоi, i ≥ 0.

Следовательно, tr |n |= ψ1 Rψ2 .rrrtr |n |= ψ2 tr |n+1 |= ψ2- yn- yn+1- yn+2- ytr |n+i |= ψ2- yn+i-r r rТАБЛИЧНЫЙ МЕТОД ВЕРИФИКАЦИИИндуктивный переход.Вариант 2. X(ψ1 Rψ2 ) ∈/ Bn+k для некоторого k, k ≥ 0.Тогда существует такое k0 , что X(ψ1 Rψ2 ) ∈/ Bn+k0 ноX(ψ1 Rψ2 ) ∈ Bn+i для любого i, 0 ≤ i < k0 .Тогда по определению графа Γϕ1 ,M в каждом множестве Bn+i ,0 ≤ i ≤ k0 , содержится формула ψ1 Rψ2 .Тогда по определению согласованных множеств ψ2 ∈ Bn+i длялюбого i, 0 ≤ i ≤ k0 , и, кроме того, ψ1 ∈ Bn+k0 .Тогда по индуктивному предположению tr |n+i |= ψ2 для любого0 ≤ i ≤ k0 и tr |n+k0 |= ψ1 .

Значит, tr |n |= ψ1 Rψ2 .rrrtr |n |= ψ2 tr |n+1 |= ψ2- yn- yn+1tr |n+k0 −1 |= ψ2- yn+2- ytr |n+k0 |= ψ1tr |n+k0 |= ψ2- y-n+kИтак, в обоих случаях ψ1 Rψ2 ∈ Bn =⇒ tr |n |= ψ1 Rψ2 .r r rТАБЛИЧНЫЙ МЕТОД ВЕРИФИКАЦИИИндуктивный переход.3.2. Покажем ψ1 Rψ2 ∈/ Bn =⇒ tr |n 6|= ψ1 Rψ2 .Пусть ψ1 Rψ2 ∈/ Bn . Т. к. ψ1 Rψ2 ∈ URSubϕ1 этой формулесоответствует некоторый цвет j.Поскольку рассматриваемый маршрут(s0 , B0 ), (s1 , B1 ), . . . , (sn , Bn ), (sn+1 , Bn+1 ), .

. .является радужным, то вершины, окрашенные в цвет j,встречаются в этом маршруте бесконечно часто.Значит, существует такое k, k ≥ 0, что вершина (sn+k , Bn+k ) —первая, окрашенная в цвет j вершина, следующая в этомрадужном маршруте вслед за вершиной (sn , Bn ).Имеются две причины, по которым вершина (sn+k , Bn+k )оказалась окрашенной в цвет j:I ψ2 ∈/ Bn+k ,I X(ψ1 Rψ2 ) ∈ Bn+k ,Рассмотрим каждый из этих случаев по отдельности.ТАБЛИЧНЫЙ МЕТОД ВЕРИФИКАЦИИИндуктивный переход.Вариант 1.

ψ2 ∈/ Bn+k .Т. к. все вершины (sn+i , Bn+i ), 0 ≤ i < k не окрашены в цвет j,для каждого из множеств Bn+i , 0 ≤ i < k, верны соотношенияψ2 ∈ Bn+iиX(ψ1 Rψ2 ) ∈/ Bn+i .Тогда по определению графа Γϕ1 ,M для каждого множестваBn+i , 0 ≤ i < k, верно соотношение ψ1 Rψ2 ∈/ Bn+i . А отсюдаследует, что ψ1 ∈/ Bn+i для любого i, 0 ≤ i < k.Тогда по индуктивному предположениюtr |n+i |= ψ2 и tr |n+i 6|= ψ1 для любого i, 0 ≤ i < k,tr |n+k 6|= ψ2 .rrrtr |n 6|= ψ1 tr |n+1 6|= ψ1tr |n |= ψ2 tr |n+1 |= ψ2- yn- yn+1tr |n+k−1 6|= ψ1tr |n+k−1 |= ψ2- y- yn+2А это означает, что tr |n 6|= ψ1 Rψ2 .tr |n+k 6|= ψ2- yn+k-r r rТАБЛИЧНЫЙ МЕТОД ВЕРИФИКАЦИИИндуктивный переход.Вариант 2.

X(ψ1 Rψ2 ) ∈ Bn+k .Т. к. все вершины (sn+i , Bn+i ), 0 ≤ i < k не окрашены в цвет j,для каждого из множеств Bn+i , 0 ≤ i < k, верны соотношенияψ2 ∈ Bn+iиX(ψ1 Rψ2 ) ∈/ Bn+i .Тогда по определению графа Γϕ1 ,M для каждого множества/ Bn+i . А отсюдаBn+i , 0 ≤ i ≤ k, верно соотношение ψ1 Rψ2 ∈следует, что ψ1 ∈/ Bn+i для любого i, 0 ≤ i < k и ψ2 ∈/ Bn+k .Тогда по индуктивному предположениюtr |n+i |= ψ2 и tr |n+i 6|= ψ1 для любого i, 0 ≤ i < k,tr |n+k 6|= ψ2 .rrrtr |n 6|= ψ1 tr |n+1 6|= ψ1tr |n |= ψ2 tr |n+1 |= ψ2- yn- yn+1tr |n+k−1 6|= ψ1tr |n+k−1 |= ψ2- y- yn+2И во втором случае tr |n 6|= ψ1 Rψ2 .tr |n+k 6|= ψ2- yn+k-r r rТАБЛИЧНЫЙ МЕТОД ВЕРИФИКАЦИИИндуктивный переход.Таким образом, если ψ1 Rψ2 ∈/ Bn , то tr |n 6|= ψ1 Rψ2 .В итоге, для любой формулы вида ψ1 Rψ2 и для любойвершины (sn , Bn ) нашего радужного маршрута верносоотношениеψ1 Rψ2 ∈ Bn ⇐⇒ tr |n |= ψ1 Rψ2 .4.

Темпоральный оператор U.Для доказательства соотношенияψ1 Rψ2 ∈ Bn ⇐⇒ tr |n |= ψ1 Rψ2применяются рассуждения, аналогичные тем, которые былииспользованы для исследования оператора R.Самостоятельно.ТАБЛИЧНЫЙ МЕТОД ВЕРИФИКАЦИИЗавершив обоснование индуктивного перехода, мы тем самымзавершили доказательство первой части теоремы:M 6|= ϕ1⇑в графе Γϕ1 ,M существует хотя бы один радужный маршрут,исходящий из вершины v0 = (s0 , B0 ), в которой s0 ∈ S0 иϕ1 ∈/ B0 .Покажем, что в том случае, когда имеет место M 6|= ϕ1 , вграфе Γϕ1 ,M из некоторой вершины v0 = (s0 , B0 ), в которойs0 ∈ S0 и ϕ1 ∈/ B0 , исходит хотя бы один радужный маршрут.ТАБЛИЧНЫЙ МЕТОД ВЕРИФИКАЦИИПусть M 6|= ϕ1 . Тогда в LTS M существует такая начальнаятрасса tr , для которой tr 6|= ϕ1 .

Рассмотрим эту трассу tr .Для каждого i, i ≥ 0, положимBi = {ψ : ψ ∈ FLSubϕ1 , tr |i |= ψ .}Согласно утверждению 4, все построенные множества Biявляются согласованными.Покажем, что последовательность пар(tr [0], B0 ), (tr [1], B1 ), (tr [2], B2 ), . . . , (tr [n], Bn ), (tr [n+1], Bn+1 ), . .

.образует искомый радужный маршрут в графе Γϕ1 .ТАБЛИЧНЫЙ МЕТОД ВЕРИФИКАЦИИДействительно,1. Для любого n, n ≥ 0, верно tr [n] −→ tr [n + 1], поскольку tr— маршрут в LTS M.2. Для любого n, n ≥ 0 и для любой формулы Xψ ∈ XSubϕ1 ,верноXψ ∈ Bn ⇐⇒ ψ ∈ Bn+1посколькуXψ ∈ Bn ⇐⇒ tr |n |= Xψ ⇐⇒ tr |n+1 |= ψ ⇐⇒ ψ ∈ Bn+1 .3. tr [0] ∈ S0 (т. к. tr — начальная трасса в M) и ϕ1 ∈/ B0 (т. к.tr |0 6|= ϕ1 ).Значит, последовательность(tr [0], B0 ), (tr [1], B1 ), (tr [2], B2 ), . . .

, (tr [n], Bn ), (tr [n+1], Bn+1 ), . . .является маршрутом в графе Γϕ1 ,M , исходящим из нужнойвершины.ТАБЛИЧНЫЙ МЕТОД ВЕРИФИКАЦИИ4. Осталось показать, что маршрут(tr [0], B0 ), (tr [1], B1 ), (tr [2], B2 ), . . . , (tr [n], Bn ), (tr [n+1], Bn+1 ), . . .является радужным.Рассмотрим произвольное число n, n ≥ 0 и произвольнуюформулу ψi ∈ URSubϕ1 .

Покажем, что существует такоеk, k ≥ 0, что вершина (tr [n + k], Bn+k ) окрашена в цвет i.ТАБЛИЧНЫЙ МЕТОД ВЕРИФИКАЦИИОграничимся рассмотрением Until-формулы ψi = χ0 Uχ2 .(Для формул вида ψi = χ0 Rχ2 доказательство проведитесамостоятельно. )1. Если tr |n 6|= X(χ1 Uχ2 ), то X(χ1 Uχ2 ) ∈/ Bn , и,следовательно, вершина (tr [n], Bn ) окрашена в цвет j.2. А если tr |n |= X(χ1 Uχ2 ), то tr |n+1 |= χ1 Uχ2 . Тогдасуществует такое k, k ≥ 1, что tr |n+k |= χ2 . Поэтомуχ2 ∈ Bn+k , и вершина (tr [n + k], Bn+k ) окрашена в цвет j.Таким образом, вершины цвета j встречаются в нашеммаршруте бесконечно часто.

Поскольку ψi была произвольной(Until-Release)-формулой, это означает, что наш маршрут вграфе Γϕ1 ,M является радужным.АЛГОРИТМ ВЕРИФИКАЦИИ МОДЕЛЕЙПРОГРАММНо как проверить, что из заданной вершины в графе Γϕ1 ,Mне исходит ни одного радужного маршрута?Ориентированный граф Γ называется сильно связным , еслидля любой пары вершин v и u в графе Γ существует маршрутиз v в u и маршрут из u в v .Всякий максимальный сильно связный подграф графа Γназывается компонентой сильной связности .Компоненту сильной связности графа (системы Хинтикки)Γϕ1 ,M будем называть радужной, если в ней содержатсявершины всех цветов.АЛГОРИТМ ВЕРИФИКАЦИИ МОДЕЛЕЙПРОГРАММТеорема.Из вершины v в графе Γϕ1 ,M исходит радужный маршрут тогдаи только тогда, когда существует маршрут , ведущий извершины v хотя бы в одну из вершин хотя бы одной радужнойкомпоненты сильной связности.Доказательство.Самостоятельно.

Здесь все очевидно.АЛГОРИТМ ВЕРИФИКАЦИИ МОДЕЛЕЙПРОГРАММИсходные данные: формула PLTL ϕ и LTSM = hAP, S, S0 , −→, ρi.1. Построить равносильную позитивную форму ϕ1 .2. Построить систему Хинтикки Γϕ1 ,M .3. Выделить множество подформул URSubϕ1 и раскраситьвершины графа Γϕ1 ,M .4. Выделить радужные компоненты сильной связности вграфе Γϕ1 ,M .5. Выделить множество V 0 всех вершин графа Γϕ1 ,M , изкоторых достижимы радужные компоненты сильнойсвязности.6. Выделить множество V 00 всех вершин (s0 , B0 ), для которойвыполняется s0 ∈ S0 , ϕ1 ∈/ B0 .7. Вычислить V = V 0 ∩ V 00 .Результат: M |= ϕ ⇐⇒ V = ∅.АЛГОРИТМ ВЕРИФИКАЦИИ МОДЕЛЕЙПРОГРАММПример.ϕ = pUqLTS M:' $s1'- iξ(s1 ) = {p} 6&s0s2?i$ξ(s2 ) = {q}%yξ(s0 ) = {p}'s3&- iξ(s3 ) = {p} 6&$s4?iξ(s4 ) = {p}%%АЛГОРИТМ ВЕРИФИКАЦИИ МОДЕЛЕЙПРОГРАММПример.ϕ = F(pUq)1.

Позитивная форма ϕ1 = pUqFLSubϕ1 = {p, ¬p, q, ¬q, pUq, X(pUq)};XSubϕ1 = {X(pUq)};URSubϕ1 = {pUq}.АЛГОРИТМ ВЕРИФИКАЦИИ2. Строим систему Хинтикки Γϕ1 ,Mi{¬p, q}6' %s1s?2i'- i{p, ¬q,6{¬p, q}{p, ¬q}- ?is1's2ϕ1 , Xϕ1 }s0{p, ¬q}is0{p, ¬q,ϕ1 , Xϕ1 }$ϕ1 , Xϕ1 }i&- i{p, ¬q} 64?sis3{p, ¬q}- is36%{p, ¬q}ϕ1 , Xϕ1 }&$ϕ1 , Xϕ1 }s4?{p, ¬q}i%АЛГОРИТМ ВЕРИФИКАЦИИ3. Раскрашиваем вершины системыΓ ϕ1 ,M{p, ¬q}y{¬p, q}6' %s1s?2y'- i{p, ¬q,6{¬p, q}- ?ys1's2ϕ1 , Xϕ1 }s0{p, ¬q}ys0{p, ¬q,ϕ1 , Xϕ1 }$ϕ1 , Xϕ1 }i&- i{p, ¬q} 64?sis3{p, ¬q}- ys36%{p, ¬q}ϕ1 , Xϕ1 }&$ϕ1 , Xϕ1 }s4?{p, ¬q}y%АЛГОРИТМ ВЕРИФИКАЦИИ4. Выделяем радужные компонентысильнойсвязности{p, ¬q}{¬p, q}y6' %s1s?2y'- i{p, ¬q,6{¬p, q}- ?ys1's2ϕ1 , Xϕ1 }s0{p, ¬q}ys0{p, ¬q,ϕ1 , Xϕ1 }$ϕ1 , Xϕ1 }i&- i{p, ¬q} 6?s4is3{p, ¬q}- ys36%{p, ¬q}ϕ1 , Xϕ1 }&$ϕ1 , Xϕ1 }s4?{p, ¬q}y%АЛГОРИТМ ВЕРИФИКАЦИИ5.

Выделяем вершины из которыхдостижимырадужные компоненты{p, ¬q}{¬p, q}y6' %s1s?2y'- y{p, ¬q,6{¬p, q}- ?is1's2ϕ1 , Xϕ1 }s0{p, ¬q}ys0{p, ¬q,ϕ1 , Xϕ1 }$ϕ1 , Xϕ1 }y&- i{p, ¬q} 6?s4is3{p, ¬q}- ys36%{p, ¬q}ϕ1 , Xϕ1 }&$ϕ1 , Xϕ1 }s4?{p, ¬q}y%АЛГОРИТМ ВЕРИФИКАЦИИ6. Ищем вершину (s0 , B) на которойопровергаетсяϕ1'{p, ¬q}{¬p, q}y6' %s1s?2y'- y{p, ¬q,6{¬p, q}- ?is1s2ϕ1 , Xϕ1 }$$ϕ1 , Xϕ1 }s0s0yy{p, ¬q}{p, ¬q,ϕ1 , Xϕ1 }&- i{p, ¬q} 6?s4is3ϕ1 , Xϕ1 }&{p, ¬q}- ys36%{p, ¬q}ϕ1 , Xϕ1 }s4?{p, ¬q}y%АЛГОРИТМ ВЕРИФИКАЦИИ МОДЕЛЕЙПРОГРАММОписанный здесь подход к верификации распределенныхпрограмм реализован в программно-инструментальной системеверификации SPIN .Модели параллельных взаимодействующих процессовописываются на языке PROMELA (Process Meta Language),снабжаются темпоральными спецификациями (PLTLформулами), а затем выполнимость этих формул проверяетсясистемой верификации SPIN .В системе SPIN применяется табличный алгоритмверификации моделей распределенных программ.

Дляповышения его эффективности используется ряд приемов:I проверка модели «на лету»;I редукции частичных порядков;I символьное представление данных и др.АЛГОРИТМ ВЕРИФИКАЦИИ МОДЕЛЕЙПРОГРАММБолее подробно о системе верификации SPIN вам расскажутКонстантин Олегович СавенковиИгорь Владимирович Конновв курсе«Верификация программ на моделях»в весеннем семестре.КОНЕЦ ЛЕКЦИИ 22ЭКЗАМЕН СОСТОИТСЯ 11ЯНВАРЯ в 10 часов.КОНСУЛЬТАЦИЯ — 10 ЯНВАРЯв 15 часов..

Свежие статьи
Популярно сейчас
Зачем заказывать выполнение своего задания, если оно уже было выполнено много много раз? Его можно просто купить или даже скачать бесплатно на СтудИзбе. Найдите нужный учебный материал у нас!
Ответы на популярные вопросы
Да! Наши авторы собирают и выкладывают те работы, которые сдаются в Вашем учебном заведении ежегодно и уже проверены преподавателями.
Да! У нас любой человек может выложить любую учебную работу и зарабатывать на её продажах! Но каждый учебный материал публикуется только после тщательной проверки администрацией.
Вернём деньги! А если быть более точными, то автору даётся немного времени на исправление, а если не исправит или выйдет время, то вернём деньги в полном объёме!
Да! На равне с готовыми студенческими работами у нас продаются услуги. Цены на услуги видны сразу, то есть Вам нужно только указать параметры и сразу можно оплачивать.
Отзывы студентов
Ставлю 10/10
Все нравится, очень удобный сайт, помогает в учебе. Кроме этого, можно заработать самому, выставляя готовые учебные материалы на продажу здесь. Рейтинги и отзывы на преподавателей очень помогают сориентироваться в начале нового семестра. Спасибо за такую функцию. Ставлю максимальную оценку.
Лучшая платформа для успешной сдачи сессии
Познакомился со СтудИзбой благодаря своему другу, очень нравится интерфейс, количество доступных файлов, цена, в общем, все прекрасно. Даже сам продаю какие-то свои работы.
Студизба ван лав ❤
Очень офигенный сайт для студентов. Много полезных учебных материалов. Пользуюсь студизбой с октября 2021 года. Серьёзных нареканий нет. Хотелось бы, что бы ввели подписочную модель и сделали материалы дешевле 300 рублей в рамках подписки бесплатными.
Отличный сайт
Лично меня всё устраивает - и покупка, и продажа; и цены, и возможность предпросмотра куска файла, и обилие бесплатных файлов (в подборках по авторам, читай, ВУЗам и факультетам). Есть определённые баги, но всё решаемо, да и администраторы реагируют в течение суток.
Маленький отзыв о большом помощнике!
Студизба спасает в те моменты, когда сроки горят, а работ накопилось достаточно. Довольно удобный сайт с простой навигацией и огромным количеством материалов.
Студ. Изба как крупнейший сборник работ для студентов
Тут дофига бывает всего полезного. Печально, что бывают предметы по которым даже одного бесплатного решения нет, но это скорее вопрос к студентам. В остальном всё здорово.
Спасательный островок
Если уже не успеваешь разобраться или застрял на каком-то задание поможет тебе быстро и недорого решить твою проблему.
Всё и так отлично
Всё очень удобно. Особенно круто, что есть система бонусов и можно выводить остатки денег. Очень много качественных бесплатных файлов.
Отзыв о системе "Студизба"
Отличная платформа для распространения работ, востребованных студентами. Хорошо налаженная и качественная работа сайта, огромная база заданий и аудитория.
Отличный помощник
Отличный сайт с кучей полезных файлов, позволяющий найти много методичек / учебников / отзывов о вузах и преподователях.
Отлично помогает студентам в любой момент для решения трудных и незамедлительных задач
Хотелось бы больше конкретной информации о преподавателях. А так в принципе хороший сайт, всегда им пользуюсь и ни разу не было желания прекратить. Хороший сайт для помощи студентам, удобный и приятный интерфейс. Из недостатков можно выделить только отсутствия небольшого количества файлов.
Спасибо за шикарный сайт
Великолепный сайт на котором студент за не большие деньги может найти помощь с дз, проектами курсовыми, лабораторными, а также узнать отзывы на преподавателей и бесплатно скачать пособия.
Популярные преподаватели
Нашёл ошибку?
Или хочешь предложить что-то улучшить на этой странице? Напиши об этом и получи бонус!
Бонус рассчитывается индивидуально в каждом случае и может быть в виде баллов или бесплатной услуги от студизбы.
Предложить исправление
Добавляйте материалы
и зарабатывайте!
Продажи идут автоматически
5076
Авторов
на СтудИзбе
455
Средний доход
с одного платного файла
Обучение Подробнее