Пост- и предварительные условия - PullRequest
Новая
       16

Пост- и предварительные условия

3 голосов
/ 19 апреля 2019

Я просто читал документацию по языку программирования Bosque и наткнулся на раздел 12 об ошибках и проверках

Мне было интересно, есть ли в C # похожая концепция для публикации и предварительных условий. При первом взгляде я подумал, что это похоже на охранные предложения, но с точки зрения языка никто не входит в метод вообще с этими предварительными условиями.

Поскольку документация довольно новая, я опубликую исходный код, о котором я говорю, здесь: 

entity Foo {
    field x: Int;

    invariant x > 0; //check whenever a Foo is constructed

    method m(y: Int): Int
        requires y >= 0; //precondition
        ensures _result_ > 0; //postcondition
    {
        check this.x - y > 0;   //sanity check - enabled on optimized builds
        assert this.x * y != 0; //diagnostic assert - only for test/debug

        return x * y;
    }
}

В C # я обычно писал бы что-то вроде этого 

internal class Foo 
{
    private int x;

    public int  m(int y)
    {
        if(y<0) //Negative guard clause
        {
            //throw an exception
        }
        //Assertions 
        int result = x * y;

        if(result<0)
        {
            //throw an exception
        }
        return result;
    }
}

Во время написания этого вопроса я сталкивался с контрактами на код в C #, которые действуют аналогично пунктам охраны, как кажется. Contract.Requires в C # больше похож на операторы check и assert внутри метода.

Итак, мой вопрос: Существует ли аналогичная концепция, которая выполняется перед входом в метод или в случае постусловия после этого?

...