>Скажи просто, «Да, норкаман». Я всё пойму.

Меня как раз беспокоит, что ты ничего не понимаешь. В такой ситуации что тебе сказать?

Понимаешь разницу между формальным доказательством корректности и повышением уверенности?

да

Поэтому пре/постусловие по сути ничего не стоит написать, но оно ничего не гарантирует. А формально доказывать корректность куска кода от точки входа к точке выхода - это нереальная задача. Одно время доказательство корректности считалось серебрянной пулей и светлым будущим. Но потом выяснилось, что в реальном проекте, реальный человек не в состоянии это сделать. Потом были надежды, что вот-вот компилятор сам научится доказывать корректность. Потом все сгинуло и оставило след лишь в парижском метро.

> Меня как раз беспокоит, что ты ничего не понимаешь.

Ты лучше побеспокойся о том, как ты сам себе придумал тезис, начал на него опираться, и уже третий пост не можешь отмотать цепочку рассуждений назад и пересмотреть свои гипотезы.

> А формально доказывать корректность куска кода от точки входа к точке выхода - это нереальная задача.

Скорее, это ты нереальный норкоман. ))

>Ты лучше побеспокойся о том, как ты сам себе придумал тезис, начал на него опираться, и уже третий пост не можешь отмотать цепочку рассуждений назад и пересмотреть свои гипотезы.

Какие гипотезы? Я тебе код привел с пре/постусловием, который падает, намекая, что может быть наличие контракта - это еще не доказательство корректности кода.

Кто говорил про «всех вокруг»? Речь шла о «всех приличных людях». Про чукчей, которые что в голову взбредут, то и пишут, речь не шла.

Тебе в школе значение терминов «предусловие» и «постусловие» не объясняли?

Норкаман? Может ты еще спросишь, является ли наличие доказательства правильности гарантией от ошибок?

Скажи просто, «Да, норкаман». Я всё пойму.

<offtop> Заглянул в твой профиль. Похоже ты тут уже 9 лет спамишь. :) Раньше ты был более позитивным человеком. А сейчас, видимо, постарел. </offtop>

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

Но потом выяснилось, что в реальном проекте, реальный человек не в состоянии это сделать.

А есть пруфы?

>Скорее, это ты нереальный норкоман. ))

Наркоман, наркоман... Опозорился и решил зараковать тред?

>А есть пруфы?

Ты много вокруг себя видишь людей, которые доказывают свой код? Или может быть слышал о таких? (я помышленное программирование имею в виду). А представь как было бы здорово: отлаживать не надо, писать юнит-тесты не надо и т.д. Но что-то не наблюдается. Если кажется, что задача легкая - докажи математическую корректность любого своего проекта или своей части в проекте при выполненных предусловиях.

> Я тебе код привел с пре/постусловием, который падает, намекая, что может быть наличие контракта - это еще не доказательство корректности кода.

Отматывай дальше. Какая затяжка навела тебя на мысль, что я где-либо утверждал такой бред?

Бросай ты эту дрянь...

Ну дык старость - не радость.

Ты много вокруг себя видишь людей, которые доказывают свой код?

Не вижу. Но может мне пора менять окружение? :)

Или может быть слышал о таких? (я помышленное программирование имею в виду).

Слышать, то слышал. Но не видел. Может я клинический неудачник?

А представь как было бы здорово: отлаживать не надо, писать юнит-тесты не надо и т.д. Но что-то не наблюдается.

Ну это может объясняться повальной неграмотностью среди программистов.

Если кажется, что задача легкая - докажи математическую корректность любого своего проекта или своей части в проекте при выполненных предусловиях.

Нет, легкой не кажется. Но это опять же ничего не доказывает. Может я баран?

Поэтому хотелось бы пруфов. Я сам нифига не верю во все эти формальные методы. Но все эти аргументы в стиле не может быть потому, что не может как-то не серьезны. Даже в SWEBOK заглядывал - там этот вопрос как-то стороной обходят.

>Отматывай дальше. Какая затяжка навела тебя на мысль, что я где-либо утверждал такой бред?

Вот тебе вся стенограмма, изучай:

Это обычная проверка валидности введённых пользователем данных. Делается в одном месте, и сразу же выводится сообщение об ошибке. Зачем такую проверку надо вглубь запихивать, не очень понятно.

Ты что, математически доказываешь корректность всех своих вычислений и поэтому проверки не ставишь? Или надеешься, что «уж дальше-то я не напартачу».

Ты что, математически доказываешь корректность всех своих вычислений и поэтому проверки не ставишь?

Ну, вообще-то все приличные люди так и делают.

Тебя не так поняли?

Очевидно же.

Я в упор не вижу связи между тезисом «все приличные люди доказывают корректность своего кода» и «пред- и постусловия не гарантируют правильности кода». Может, покажешь уже, наконец?

И да, не «поняли», а «понял». Ты, ведь, пока у нас в единственном числе.

> «пред- и постусловия не гарантируют правильности кода».

Точнее, «пред- и постусловия гарантируют правильность кода». Я уже запутался в том, что ты мне понаприписывал.

>Слышать, то слышал. Но не видел.

Это как с пришельцами. Все мы слышали о них, но...

Ну это может объясняться повальной неграмотностью среди программистов.

Если бы можно было хоть как-то применить на практике, это в институте бы еще давали. Но, по-моему, это в программы не входит даже.

Но все эти аргументы в стиле не может быть потому, что не может как-то не серьезны.

Возможно потому, что в продакшене добиваются приемлемого качества менее затратными средствами. Иначе и языки для разработки были бы другие. У меня пруфов нет в общем, только мнение)

>Может, покажешь уже, наконец?

Показываю, следи за руками. Сначала ты сказал, что доказываешь корректность, а потом выяснилось, что под формальным доказательством корректности, ты имел в виду не доказательство вороха теорем, а расстановку контрактов в коде (http://www.linux.org.ru/jump-message.jsp?msgid=6013294&cid=6016308). Я счел своим гражданским долгом предупредить, что ты глубоко заблуждаешься. Ты решил, что это я глубоко заблуждаюсь, и вот мы нудим на эту тему.

>И да, не «поняли», а «понял». Ты, ведь, пока у нас в единственном числе.

Не, нас легион.

> под формальным доказательством корректности, ты имел в виду не доказательство вороха теорем, а расстановку контрактов в коде

Я и говорю, норкоман. Где я такое утверждал?

Вас-то легион, да только такой фантазер пока что ты один.

Но, по-моему, это в программы не входит даже

Хм. У нас было что-то такое. Там про всякие Z-notation было. Честно - нифиша не понял как это реально применить в моих задачах. Препод был не очень адекватный и на мои вопросы отвечал дескать, математику учить надо.

Возможно потому, что в продакшене добиваются приемлемого качества менее затратными средствами.

Ну как бы не боги горшки обжигают. Большиснтво делают так, как научились. Как надо, вопрос скорее всего открытый. Хотя я склоняюсь, что таки да, есть менее затратные способы.

>Я и говорю, норкоман. Где я такое утверждал?

Я и ссылку специально привел, где ты предусловия начал поминать, в ответ на теоремы. Если же ты не в контексте формального доказательства, а просто так брякнул, то расскажи как ты на самом деле доказываешь корректность своих программ? Не томи. Впрочем, подозреваю, что самый убедительный твой аргумент сводится к наркоману.

> Я и ссылку специально привел, где ты предусловия начал поминать, в ответ на теоремы.

И что?

Если же ты не в контексте формального доказательства, а просто так брякнул

Вот мне интересно, если ты имеешь хоть малейшее представление о формальном доказательстве, как ты мог спутать пред- и постусловия с проверкой входящих аргументов и возвращаемого результата?
Либо ты его не имел, либо вещества.

расскажи как ты на самом деле доказываешь корректность своих программ?

Чё рассказывать-то? Индукция + конечные автоматы. Это, конечно, не совсем «наркоман», но что-то близкое...

> Препод был не очень адекватный и на мои вопросы отвечал дескать, математику учить надо.

Только неадекватный человек посоветует учить математику. Ага-ага.

Видимо ты задавал тупые вопросы с очевидными для учивших математику людей ответами.

Брэкпоинт.

В православных языках вроде C# есть такая хорошая штука как auto property:

class Point
{
  public Point() { }

  public Point(int x, int y)
  {
    X = x;
    Y = y;
  }

  public int X { get; set; }
  public int Y { get; set; }
}

Если в будущем я захочу поменять, допустим, логику присваивания координат, мне нужно будет лишь написать геттер и сеттер, а интерфейс класса останется нетронутым.

Это не хорошая штука, а поощрение нарушения инкапсуляции разработчиками языка.

Нет абсолютно никакой разницы между подобными properties и использованием обычных структур. Ни то, ни другое не имеет никакого отношения к ООП, только в случае с set/get еще и захламляется код лишними бесполезными конструкциями.

Это не хорошая штука, а поощрение нарушения инкапсуляции разработчиками языка.

Нарушение инкапсуляции - это выпячить данные наружу, как советуют тут некоторые адепты plain C, называя это POD и, почему-то, радуясь.

Нет абсолютно никакой разницы между подобными properties и использованием обычных структур.

Чукча не читатель, чукча - писатель? Я же ясно сказал, если я захочу прикрутить какую-либо логику, мне не нужно будет ломать интерфейс (в случае со свойствами), а без свойств - будет лажа.

Ни то, ни другое не имеет никакого отношения к ООП, только в случае с set/get еще и захламляется код лишними бесполезными конструкциями.

Лишними бесполезными конструкциями захламлён, к сожалению, ваш моск.

И раз уже все приводят пример с точкой, то и я отмечусь. Сравните два класса:

class BadPoint
{
public:

  Point (unsigned int x, unsigned int y)
  : m_x(x), m_y(y) {}

  unsigned int getX() const { return m_x; }
  unsigned int getY() const { return m_y; }
  void setX (unsigned int x) { m_x = x; }
  void setY (unsigned int y) { m_y = y; }

private:

  unsigned int m_x, m_y;
};

class GoodPoint
{
public:

  Point (unsigned int x, unsigned int y)
  : m_x(x), m_y(y) {}

  unsigned int getX() const { return m_x; }
  unsigned int getY() const { return m_y; }
  void moveTo (unsigned int y, unsigned int y) { ... }

private:

  unsigned int m_x, m_y;
};

Чувствуете разницу? Первый «класс» - это пара интов с сеттерами/геттерами. Второй - действительно класс с набором методов, которые изменяют его состояние. Отличие не только в одном методе, а в самом подходе к проектированию: в первом случае к данным прилепляем какой-нибудь интерфейс, а во-втором - от интерфейса проектируем реализацию.

Хотя если честно, я обычно подобные объекты делаю иммутабельными.

P.S. Чтобы не допускать точек с отрицательными координатами, достаточно объявить их unsigned - очевидно же. Попытаетесь смешивать signed/unsigned - компилятор сразу же выдаст warning.

>Нарушение инкапсуляции - это выпячить данные наружу, как советуют тут некоторые адепты plain C, называя это POD и, почему-то, радуясь

Это не адепты plain C, а люди, искренне недоумевающие - зачем писать геттеры/сеттеры, если можно написать обычную сишную структурку, т.к. РАЗНИЦЫ НЕТ?

Я же ясно сказал, если я захочу прикрутить какую-либо логику, мне не нужно будет ломать интерфейс

setX/setY - это не интерфейс. Такое нужно ломать сразу же, а написавшему - утюгом по пальцам.

Лишними бесполезными конструкциями захламлён, к сожалению, ваш моск.

Аргументация ок

Чувствуете разницу?

Ммм...

class Point
{
  private uint _x, _y;

  Point() { }

  Point(uint x, uint y)
  {
    X = x;
    Y = y;
  }

  public uint X
  {
    get { return _x; }
    set { MoveTo(_x, value); }
  }

  public uint Y
  {
    get { return _y; }
    set { MoveTo(value, _y); }
  }
  
  public void MoveTo(uint x, uint y)
  {
    _x = x;
    _y = y;
  }
}

Это не адепты plain C, а люди, искренне недоумевающие - зачем писать геттеры/сеттеры, если можно написать обычную сишную структурку, т.к. РАЗНИЦЫ НЕТ?

В теме вообще-то речь про ООП идёт. И про то, что хорошо, когда не нужно менять интерфейс классов при каждом чихе.

setX/setY - это не интерфейс. Такое нужно ломать сразу же, а написавшему - утюгом по пальцам.

Это именно интерфейс и никак иначе.

Только X и Y выпячены наружу.

>В теме вообще-то речь про ООП идёт.

Одно из ключевых свойств ООП - это инкапсуляция. Get/set её нарушают

Только X и Y выпячены наружу.

Нет. Комилятор сам создаст приватные поля для них. А то, что ты видишь - это два метода: геттер и сеттер, суть - интерфейс.

Вот радует меня лор в плане додумывания ситуации, где твой оппонент оказывается обязательно дебилом. Тьфу на вас на всех.

> А то, что ты видишь - это два метода: геттер и сеттер, суть - интерфейс.

Интерфейс прочитать число/записать число уже есть - это обычное поле, «торчащее наружу». Смысл дублировать уже существующую функциональность?

Ты до сих пор задаёшь вопросы, на которые ответ - очиведен (да-да, если ты учил «математику»)

Интерфейс прочитать число/записать число уже есть - это обычное поле, «торчащее наружу». Смысл дублировать уже существующую функциональность?

Для тех, кто почему-то медленно соображает, повторяю третий раз: если я захочу вставить какую-либо логику работу с этими полями (например, бросать исключение для значений меньше нуля, или что-то другое), я просто допишу геттер и сеттер. При этом интерфейс класса не изменится.

> я просто допишу геттер и сеттер. При этом интерфейс класса не изменится.

Поменяется поведение, название метода не будет отражать его суть, присутствующий изначально инвариант setX(1); getX() == 1 - уже не будет выполняться.

1) http://ru.wikipedia.org/wiki/%D0%9F%D1%80%D0%B8%D0%BD%D1%86%D0%B8%D0%BF_%D0%B...

2) Один из базовых принципов ООП - data abstraction. Объект не должен выставлять детали своей реализации

А что толку, что интерфейс не изменится? Ну какая от этого практическая польза? Ну не было твоей проперти, я бы и так все отрефакторил. Вы о мелочах каких-то спорите.

Поменяется поведение, название метода не будет отражать его суть, присутствующий изначально инвариант setX(1); getX() == 1 - уже не будет выполняться.

Кто тебе такую ересь сказал? Где ты это вообще вычитал? Может я assert хочу туда вставить?

Один из базовых принципов ООП - data abstraction. Объект не должен выставлять детали своей реализации

Вот именно. Вы сами себе противоречите.

А что толку, что интерфейс не изменится? Ну какая от этого практическая польза? Ну не было твоей проперти, я бы и так все отрефакторил. Вы о мелочах каких-то спорите.

Если это твой код - можешь отрефакторить без проблем. Если это код какой-нить библиотеки - не можешь. Вернее, как... можешь, конечно, но тогда также отрефакторить прийдётся все другие приложения, на эту библиотеку завязанные.

Да, для библиотеки я так не стал бы джедайствовать.

>Только X и Y выпячены наружу.

У тебя тоже наружу выпячены на чтение - это детали реализации или нет? Чем move( x, y ) принципиально лучше set_x/set_y ?

>Поменяется поведение, название метода не будет отражать его суть, присутствующий изначально инвариант setX(1); getX() == 1 - уже не будет выполняться.

Если 1 - валидное значение для X, то инвариант выполняться будет. Если невалидное, то это какой-то вредный инвариант. А в случае структуры - пиши что хочешь, кто хочешь. Теперь в любом месте, куда прилетит такой объект, по-хорошему нужно первым делом контролировать, не случилось ли с ним чего страшного. Или понадеяться, что все будет в порядке.

мне это кажется странным, но спорить не буду, ибо я в другой области работаю