Здравствуйте, reductor, Вы писали:
R>Вы, мне кажется, путаете две близкие вещи. R>Посмотрим, вот ваша функция на Haskell, где вообще нет оператора выхода: R>
R>contains _ [] = False
R>contains y (x:xs) | x == y = True
R> | otherwise = contains y xs
R>
R>1-в-1, То же самое. R>А вот функция, которая пытается сделать сразу 10 вещей закрывая дыры в логике преждевременным выходом так легко формальным образом не выразится. Можно делать выводы.
R>Несколько выходов — это всегда повод к тому, чтобы задать себе вопрос — не создаю ли я тут эмуляцию вложеных функций. И ответить на этот вопрос или утвердительно или отрицательно. R>А все остальное уже из этого следует.
Я, как раз, ничего не путаю. Чтобы адекватно обмениваться мнениями, немного терминологии:
goto, continue, break, return — суть операторы безусловного перехода. return — это, грубо, безусловный переход на метку конца подпрограммы.
На блок-диаграммах алгоритмов все операторы безусловного перехода обозначаются одинаково и имеют один и тот же смысл. В приведенной мною блок-диаграмме нехватает блока {конец}, куда я должен был привести алгоритм после присвоения выходного значения.
Такие разновидности goto как continue, break, return позволяют банально обходится без меток, используя границы блоков в структурном программировании.
И кстати, то о чем говоришь ты, легко достигается и без множественного return, и причина в этом другая/другие. Ты намекал на кашу в построении алгоритма конкретной процедуры. Для каши в голове может быть миллион причин, и оно не лечится сведением ретурнов к единственности. Да и вообще, с т.з. структурного программирования это не принципиально. Гораздо принципиальней внешний интерфейс самой процедуры и спецификация ее семантики. Дай бог обойтись без каши на этом уровне.
---------
Да, и что там насчет останова автомата Тьюринга, что не так? Мы же не перепрыгиваем через уровни во время return, более того, return стоит именно рассматривать как оператор безусловного перехода на том же уровне вложенности. В отличие от exceptions... Вот уж где Тьюринг отдыхает... ИМХО, другие модели нынче требуются, малость посложнее, для формального описания сути происходящего в современном ПО.
---------
И еще, насчет твоего примера на Haskell. А что, в этом ЯП есть оператор goto?
Я когда-то возился с Прологом, поэтому примерно понял, о чем речь в твоем отрезке (с Haskell не знаком). Однако, в том же Прологе, такая частоиспользуемая штука, как отсекающие условия — что как не разновидность return?
В твоем примере вот это оно: "x == y = True", самый что ни на есть немедленный return из алгоритма, как только попали в подходящую для return ситуацию.
Здравствуйте, reductor, Вы писали:
>>> Что касается выхода из циклов по флагам и отсутствия break, то вообще >>> не понимаю в чем проблема — что мешает вынести цикл в отдельную >>> функцию и выходить исключительно из цикла, делая код более предсказуемым?
C>>Слишком много переменных может потребоваться передавать в виде параметров.
R>Ну наверное может. А может и нет. Или наоборот. О чем вообще мы?
О том, что ты вот только сейчас начинаешь более-менее четко определять свою позицию. Насчет выхода из цикла или из "всей" подпрограммы — ты сделал правильное замечание. И тебя тоже весьма правильно поправили насчет целесообразности в случае сильной связанности кода цикла с окружающим кодом.
C>>Нет уж, сами затеяли спор — сами и показывайте код, который C>>множественный выход делает недоказуемым и вообще отстойным.
R>Извините, это вы говорите, что у вас есть такой код. Что он есть у меня, я не говорил. R>А я такого кода не пишу.
R>Будем продолжать беседы о том сколько ангелов уместится на острие иголки?
Нет, лучше сместиться в сторону верифицирования современного ПО. Ты хоть представляешь, КАК ИМЕННО оно происходит сейчас? В общем, твоя точка зрения понятна, но она неприменима на "реальных объемах".
R>Или я говорил, что код с несколькими стейтментами return не может работать корректно? R>или что его нельзя в AST трансформировать во что-то там? Или что его нельзя скомпилировать? R>Я утверждал, что без явной обработки всех условий вероятность ошибки и последующая с этим возня могут возрасти многократно.
Все с точностью до наоборот. В сочетании с RAII это помогает писать очень простой код. А надежность ПО достигается косвенным путем, а именно — чем проще код, тем сложнее ошибиться, тем легче сопровождать/исправлять и верифицировать.
Теперь представь себе гору кода, если бы мы делал все через if-else и явное управление ресурсами... бррр... Вероятность ошибки возрасла бы многократно. Т.е., дело в том, что некое ELSE все равно выполняется. И разработчик, размеется, прекрасно знает — что именно (вызов деструкторов локальных объектов). И он это использует на всю катушку, для однократного программирования кода этих ELSE и затем многократного повторного использования (да и еще автоматического). Это тебе как бы затравка на другие способы повышения надежности (читабельность, максимальное повторное использование)
А с использованием exceptions, код выглядит еще читабельнее:
Здравствуйте, vdimas, Вы писали:
V>Здравствуйте, reductor, Вы писали:
R>>Вы, мне кажется, путаете две близкие вещи. R>>Посмотрим, вот ваша функция на Haskell, где вообще нет оператора выхода: R>>
R>>contains _ [] = False
R>>contains y (x:xs) | x == y = True
R>> | otherwise = contains y xs
R>>
R>>1-в-1, То же самое. R>>А вот функция, которая пытается сделать сразу 10 вещей закрывая дыры в логике преждевременным выходом так легко формальным образом не выразится. Можно делать выводы.
R>>Несколько выходов — это всегда повод к тому, чтобы задать себе вопрос — не создаю ли я тут эмуляцию вложеных функций. И ответить на этот вопрос или утвердительно или отрицательно. R>>А все остальное уже из этого следует.
V>Я, как раз, ничего не путаю. Чтобы адекватно обмениваться мнениями, немного терминологии: V>goto, continue, break, return — суть операторы безусловного перехода. return — это, грубо, безусловный переход на метку конца подпрограммы.
V>На блок-диаграммах алгоритмов все операторы безусловного перехода обозначаются одинаково и имеют один и тот же смысл. В приведенной мною блок-диаграмме нехватает блока {конец}, куда я должен был привести алгоритм после присвоения выходного значения.
V>Такие разновидности goto как continue, break, return позволяют банально обходится без меток, используя границы блоков в структурном программировании.
Все гораздо проще. Есть, предположим, спецификация, вида:
| Positive if x > 0
f(x) = | Negative if x < 0
| Zero otherwise
Не может быть спецификации без _полной_ проверки возможных значений.
И, строго говоря, код вида:
int f (int x) {
if (x > 0) return 1;
if (x < 0) return -1;
return 0;
}
Ей формально не соответствует. И главное, что проверить это очень сложно. В общем виде такое вообще не проверяется.
А когда таких вариантов много, то непредсказуемость растет очень быстро.
тогда как код вида:
int f (int x) {
if (x > 0) return 1;
else if (x < 0) return -1;
else return 0;
}
Вполне соответствует. Проверяются все значения и для любого варианта есть выход. То есть можно показать, что эта функция соответствует спецификации. Речь формально уже не идет о множественном выходе.
V>--------- V>Да, и что там насчет останова автомата Тьюринга, что не так? Мы же не перепрыгиваем через уровни во время return, более того, return стоит именно рассматривать как оператор безусловного перехода на том же уровне вложенности. В отличие от exceptions... Вот уж где Тьюринг отдыхает... ИМХО, другие модели нынче требуются, малость посложнее, для формального описания сути происходящего в современном ПО.
Проблема с тьюринг-полным автоматом в том, что мы не можем определить свойства программы, у которой есть внешний вход.
Потому, мы вынуждены так или иначе с одной стороны определять то, что можем и с другой ограничивать используемые конструкции.
Именно потому go to statements considered harmful.
Что касается отдыхает тьюринг или нет, то вообще Машина Тьюриннга может вычислить _любую_ вычислимую функцию.
И все остальные выч. модели, которые могут эмулировать МТ ей равномощны.
Но дело не в этом. Для формализации и доказательств действительно используется типизированное лямбда-исчисление и изоморфизм Карри-Говарда. http://en.wikipedia.org/wiki/Curry-Howard_isomorphism
Которое, являсь само по себе формальной математической моделью проще отображается в регулярную математику и обратно.
К слову что я Хаскель вспомнил.
V>--------- V>И еще, насчет твоего примера на Haskell. А что, в этом ЯП есть оператор goto?
Нет конечно. И return нет. И циклов нет. И присваиваний нет. Переменных нет.
Потому очень показателен пример на нем. Я вообще часто, когда что-то сложное пишу на любом языке, сначала на хаскеле спецификацию-прототип составляю (Это если нельзя по каким-то причинам сразу на хаскеле написать.
V>Я когда-то возился с Прологом, поэтому примерно понял, о чем речь в твоем отрезке (с Haskell не знаком). Однако, в том же Прологе, такая частоиспользуемая штука, как отсекающие условия — что как не разновидность return?
Тем, что задается соответсвие между входом и выходом. скажем так, справедливо сказать, что этот _выразим_ с помощью return. Как и return с помощью джампа куда-нибудь. Но не оставляет вариантов для размышления.
V>В твоем примере вот это оно: "x == y = True", самый что ни на есть немедленный return из алгоритма, как только попали в подходящую для return ситуацию.
Нет конечно. Это именно что задание соответствия между выходом и выходом. Чего в функции на Си может и не быть явным (определяемым анализатором) образом.
Здравствуйте, vdimas, Вы писали:
R>>Ну наверное может. А может и нет. Или наоборот. О чем вообще мы?
V>О том, что ты вот только сейчас начинаешь более-менее четко определять свою позицию. Насчет выхода из цикла или из "всей" подпрограммы — ты сделал правильное замечание. И тебя тоже весьма правильно поправили насчет целесообразности в случае сильной связанности кода цикла с окружающим кодом.
Ну лично я о том, что без примеров это как беседа о марсианах.
V>Нет, лучше сместиться в сторону верифицирования современного ПО. Ты хоть представляешь, КАК ИМЕННО оно происходит сейчас? В общем, твоя точка зрения понятна, но она неприменима на "реальных объемах".
Я? представляю, а что?
А можно ли услышать что такое "реальные объемы"? А то может у меня какие-то они нереальные, мало ли.
И почему даже если так, то нужно делать код менее верифицируемым, чем можно?
Здравствуйте, vdimas, Вы писали:
V>Здравствуйте, reductor, Вы писали:
R>>Или я говорил, что код с несколькими стейтментами return не может работать корректно? R>>или что его нельзя в AST трансформировать во что-то там? Или что его нельзя скомпилировать? R>>Я утверждал, что без явной обработки всех условий вероятность ошибки и последующая с этим возня могут возрасти многократно.
V>Все с точностью до наоборот. В сочетании с RAII это помогает писать очень простой код. А надежность ПО достигается косвенным путем, а именно — чем проще код, тем сложнее ошибиться, тем легче сопровождать/исправлять и верифицировать.
V>Например, в С++, опять ресурсы и коды возвратов:
Ну если дело только в этом конкретном коде, то:
if (error( openRes1() )) return ERR_RESOURCE1;
else if (error( openRes2() )) return ERR_RESOURCE2;
else if (error( openRes3() )) return ERR_RESOURCE3;
else return ERR_SUCCESS;
формальнее некуда
V>Теперь представь себе гору кода, если бы мы делал все через if-else и явное управление ресурсами... бррр... Вероятность ошибки возрасла бы многократно. Т.е., дело в том, что некое ELSE все равно выполняется. И разработчик, размеется, прекрасно знает — что именно (вызов деструкторов локальных объектов). И он это использует на всю катушку, для однократного программирования кода этих ELSE и затем многократного повторного использования (да и еще автоматического). Это тебе как бы затравка на другие способы повышения надежности (читабельность, максимальное повторное использование)
если else есть, а он есть всегда, когда мы имеем любое соответствие между входом и выходом, то явное его присутствие хуже не сделает. а наоборот — может сделать еще и заметными свои ошибки в понимании того, как эта функция должна себя вести.
когда вдруг понимаешь, что в else нечего писать, порой настоящее просветление получаешь.
V>А с использованием exceptions, код выглядит еще читабельнее:
А вот на иксепшены я и не гнал. Тут где-то даже валяется постинг от меня в их защиту.
правда их я люблю не в варианте с++, но это уже детали.
Здравствуйте, IT, Вы писали:
IT>...переписать вот такой код без returns?
public class ResultException<T> : ApplicationException
{
public T Result;
public ResultException(T result)
{
Result = result;
}
}
public class UndefinedResultException : ApplicationException
{
}
private static MemberMapper GetNullableMemberMapper(MapMemberInfo mi)
{
try
{
Type type = mi.MemberAccessor.Type;
if (type.IsGenericType == false || mi.MapValues != null)
throw new ResultException<MemberMapper>(null);
Type underlyingType = Nullable.GetUnderlyingType(type);
if (underlyingType == null)
throw new ResultException<MemberMapper>(null);
if (underlyingType.IsEnum)
{
underlyingType = Enum.GetUnderlyingType(underlyingType);
if (underlyingType == typeof(SByte)) throw new ResultException<MemberMapper>(new NullableSByteMapper. Enum());
if (underlyingType == typeof(Int16)) throw new ResultException<MemberMapper>(new NullableInt16Mapper. Enum());
if (underlyingType == typeof(Int32)) throw new ResultException<MemberMapper>(new NullableInt32Mapper. Enum());
if (underlyingType == typeof(Int64)) throw new ResultException<MemberMapper>(new NullableInt64Mapper. Enum());
if (underlyingType == typeof(Byte)) throw new ResultException<MemberMapper>(new NullableByteMapper. Enum());
if (underlyingType == typeof(UInt16)) throw new ResultException<MemberMapper>(new NullableUInt16Mapper.Enum());
if (underlyingType == typeof(UInt32)) throw new ResultException<MemberMapper>(new NullableUInt32Mapper.Enum());
if (underlyingType == typeof(UInt64)) throw new ResultException<MemberMapper>(new NullableUInt64Mapper.Enum());
}
else
{
if (underlyingType == typeof(SByte)) throw new ResultException<MemberMapper>(new NullableSByteMapper());
if (underlyingType == typeof(Int16)) throw new ResultException<MemberMapper>(new NullableInt16Mapper());
if (underlyingType == typeof(Int32)) throw new ResultException<MemberMapper>(new NullableInt32Mapper());
if (underlyingType == typeof(Int64)) throw new ResultException<MemberMapper>(new NullableInt64Mapper());
if (underlyingType == typeof(Byte)) throw new ResultException<MemberMapper>(new NullableByteMapper());
if (underlyingType == typeof(UInt16)) throw new ResultException<MemberMapper>(new NullableUInt16Mapper());
if (underlyingType == typeof(UInt32)) throw new ResultException<MemberMapper>(new NullableUInt32Mapper());
if (underlyingType == typeof(UInt64)) throw new ResultException<MemberMapper>(new NullableUInt64Mapper());
if (underlyingType == typeof(Char)) throw new ResultException<MemberMapper>(new NullableCharMapper());
if (underlyingType == typeof(Single)) throw new ResultException<MemberMapper>(new NullableSingleMapper());
if (underlyingType == typeof(Boolean)) throw new ResultException<MemberMapper>(new NullableBooleanMapper());
if (underlyingType == typeof(Double)) throw new ResultException<MemberMapper>(new NullableDoubleMapper());
if (underlyingType == typeof(DateTime)) throw new ResultException<MemberMapper>(new NullableDateTimeMapper());
if (underlyingType == typeof(Decimal)) throw new ResultException<MemberMapper>(new NullableDecimalMapper());
if (underlyingType == typeof(Guid)) throw new ResultException<MemberMapper>(new NullableGuidMapper());
}
throw new ResultException<MemberMapper>(null);
}
catch (ResultException<MemberMapper> re)
{
return re.Result;
}
throw new UndefinedResultException();
}
СГ>PROCEDURE TransferMoney (src, dst: Account; m: Money; log: Log): BOOLEAN;
СГ> VAR r: BOOLEAN; t: Transaction; s, d: LockedAccount; x: Transfer;
СГ> PROCEDURE BeginTransfer;
СГ> BEGIN(*...*)
СГ> END BeginTransfer;
СГ> PROCEDURE GetMoney (): BOOLEAN;
СГ> BEGIN(*...*)
СГ> END GetMoney;
СГ> PROCEDURE AddMoney (): BOOLEAN;
СГ> BEGIN(*...*)
СГ> END AddMoney;
СГ> PROCEDURE Enroll (a: Account; OUT b: LockedAccount): BOOLEAN;
СГ> BEGIN(*...*)
СГ> END Enroll;
СГ> PROCEDURE Commit (): BOOLEAN;
СГ> BEGIN(*...*)
СГ> END Commit;
СГ> PROCEDURE EndTransfer;
СГ> BEGIN(*...*)
СГ> END EndTransfer;
СГ>BEGIN r := (src # NIL) & (dst # NIL) & (m > 0);
СГ> IF r THEN
СГ> BeginTransfer;
СГ> r := Enroll(src, s) & Enroll(dst, d) & GetMoney() & AddMoney() & Commit();
СГ> EndTransfer
СГ> END;
СГ> RETURN r
СГ>END TransferMoney;
СГ>
Данные у нас правильные по определению, функция enroll на заблокированную базу данных нарваться не может опять же по определению. Rollback не бывает. Об остальном я, пожалуй, промолчу.
Здравствуйте, Cyberax, Вы писали:
C>Да, напомните мне, плиз, почему в Java/C# есть OutOfMemoryException
Не знаю, как с C#, а в Java есть только OutOfMemoryError. По документации, исключения(?) типа Error приложения не должны перехватывать и, если перехватывают, должны передавать наверх.
[]
R>Все гораздо проще. Есть, предположим, спецификация, вида:
R>
R> | Positive if x > 0
R>f(x) = | Negative if x < 0
R> | Zero otherwise
R>
R>Не может быть спецификации без _полной_ проверки возможных значений. R>И, строго говоря, код вида: R>
R>int f (int x) {
R> if (x > 0) return 1;
R> if (x < 0) return -1;
R> return 0;
R>}
R>
R>Ей формально не соответствует. И главное, что проверить это очень сложно. В общем виде такое вообще не проверяется.
Если этот код формально не соответствует той спецификации, то видимо он формально соответствует некой другой спецификации. Можно взглянуть на нее?
R>А когда таких вариантов много, то непредсказуемость растет очень быстро. R>тогда как код вида: R>
R>int f (int x) {
R> if (x > 0) return 1;
R> else if (x < 0) return -1;
R> else return 0;
R>}
R>
R>Вполне соответствует. Проверяются все значения и для любого варианта есть выход. То есть можно показать, что эта функция соответствует спецификации. Речь формально уже не идет о множественном выходе.
Почти уверен, что на языке промежуточного представления, которым пользуется нормальный компилятор (SSA или чего там еще), оба эти варианта выглядят одинаково.
Здравствуйте, Костя Ещенко, Вы писали:
КЕ>Здравствуйте, reductor, Вы писали:
КЕ>[]
КЕ>Если этот код формально не соответствует той спецификации, то видимо он формально соответствует некой другой спецификации. Можно взглянуть на нее?
Не понял. Какой еще спецификации?
А вообще я бы тоже глянул на ту спецификацию, которая заставляет писать такой код.
КЕ>Почти уверен, что на языке промежуточного представления, которым пользуется нормальный компилятор (SSA или чего там еще), оба эти варианта выглядят одинаково.
Скорее всего, с этим простым примером так и будет. Что с того? Да и какая вообще разница во что это потом превратится?
xBlackCat wrote:
> C>Да, напомните мне, плиз, почему в Java/C# есть OutOfMemoryException > Не знаю, как с C#, а в Java есть только OutOfMemory*Error*. По > документации, исключения(?) типа Error приложения не должны > перехватывать и, если перехватывают, должны передавать наверх.
Перехватить его можно, но опасно — при любом new оно может вылететь
снова. Хотя я видел системы, где OOM успешно обрабатывался.
Здравствуйте, reductor, Вы писали:
КЕ>>Если этот код формально не соответствует той спецификации, то видимо он формально соответствует некой другой спецификации. Можно взглянуть на нее?
R>Не понял. Какой еще спецификации?
ты приводил эту:
| Positive if x > 0
f(x) = | Negative if x < 0
| Zero otherwise
R>А вообще я бы тоже глянул на ту спецификацию, которая заставляет писать такой код.
Вот и мне интересно — если код соответствует спецификации, только являясь ее достаточно точной калькой — то как может выглядеть спецификация "некрасивого" варианта? Есть варианты?
КЕ>>Почти уверен, что на языке промежуточного представления, которым пользуется нормальный компилятор (SSA или чего там еще), оба эти варианта выглядят одинаково.
R>Скорее всего, с этим простым примером так и будет. Что с того?
Всего лишь то, что эти примеры эквивалентны с точки зрения формальных преобразований над кодом, и аргументы насчет сложности верификации, ИМХО, мимо кассы. Имеют значение лишь удобство восприятия и внесения изменений человеком.
R>Да и какая вообще разница во что это потом превратится?
Здравствуйте, Костя Ещенко, Вы писали:
КЕ>Вот и мне интересно — если код соответствует спецификации, только являясь ее достаточно точной калькой — то как может выглядеть спецификация "некрасивого" варианта? Есть варианты?
Нет, у меня вариантов нет. И вообще пример был для описания различий между формальной реализацией и неформальной.
КЕ>>>Почти уверен, что на языке промежуточного представления, которым пользуется нормальный компилятор (SSA или чего там еще), оба эти варианта выглядят одинаково.
R>>Скорее всего, с этим простым примером так и будет. Что с того?
КЕ>Всего лишь то, что эти примеры эквивалентны с точки зрения формальных преобразований над кодом, и аргументы насчет сложности верификации, ИМХО, мимо кассы. Имеют значение лишь удобство восприятия и внесения изменений человеком.
Я скоро это внесу себе в сигнатуру:
Корректная работа кода не означает автоматически, что код выполняет то, что предполагалось. Это так же не означает что код соответствует спецификации и, соответственно, что можно считать его доказаным или хотя бы без багов.
Ошибки в софте, написанном десятилетия назад и обнаруженные только сейчас это непосредственным образом подтверждают. Код с явной обработкой всех условий будет с меньшей вероятностью подвержен глупым ошибкам, чем код без таковой.
Что еще?
P.S
Еще у меня есть все основания предполагать, что код, написанный формальным образом читается и понимается гораздо легче, чем наоборот. По крайней мере человеком, у которого все в порядке с логикой. Это эмпирический вывод. Доказать я это не могу.
P.P.S
иксепшенов это не касается, они — совершенно другая тема.
Здравствуйте, reductor, Вы писали:
R>Корректная работа кода не означает автоматически, что код выполняет то, что предполагалось. Это так же не означает что код соответствует спецификации и, соответственно, что можно считать его доказаным или хотя бы без багов.
Корректно работающий в соответствии со спецификацией код совсем не обязательно выполняет то, что предполагалось.
Это эмпирический вывод, основывающийся на том, что:
a) спецификации так же содержат ошибки;
b) заказчик может не суметь четко описать свои пожелания и ожидания.
Доказать я его не могу.
... << RSDN@Home 1.1.4 stable rev. 510>>
SObjectizer: <микро>Агентно-ориентированное программирование на C++.
Так вот Мейер в качестве одной из дисциплин обработки исключений определяет "Повторение" (Retrying), но об этом чуть ниже.
Жаль, но там нет ссылки на онлайн версию... В наших магазинах я такой книги не видал.
E>Сдается мне, что мы сейчас говорим об одном и том же, но разными словами.
Да. Точно, мы говорим об одном и том-же.
Просто в начале, я решил, что ты предлагаеш иногда использовать исключения на одном логическом уровне для передачи информации/контроля (как тот пример с курсором и короткой строкой).
Теперь всё ясно.
Здравствуйте, eao197, Вы писали:
E>Здравствуйте, reductor, Вы писали:
R>>Корректная работа кода не означает автоматически, что код выполняет то, что предполагалось. Это так же не означает что код соответствует спецификации и, соответственно, что можно считать его доказаным или хотя бы без багов.
E>Корректно работающий в соответствии со спецификацией код совсем не обязательно выполняет то, что предполагалось.
Корректно работающий в соответствии со спецификацией код, делает то, что предполагалось в спецификации с несколько большей вероятностью, чем код, который ей не соответствует. И есть формальный аппарат, позволяющий это проверить.
Если есть данные или другой аппарат, позволяющие это оспорить и доказать, что наоборот — буду рад услышать.
E>Это эмпирический вывод, основывающийся на том, что: E>a) спецификации так же содержат ошибки; E>b) заказчик может не суметь четко описать свои пожелания и ожидания. E>Доказать я его не могу.
А вот это уже лирика, к делу не относящаяся. Методов, чтобы определить в каком состоянии писал заказчик спецификацию и писал ли вообще, а не сгенерировал генератором матерных слов, я не знаю. Себе спецификации я стараюсь писать сам. Формальные и без противоречий (это очень просто).