On Sat, Feb 14, 2015 at 8:19 AM, Yasuo Ohgaki <yohg...@ohgaki.net> wrote:

>      myMethod() {
>           require(MyMethod());
>      }
>

My hand is not used to new syntax yet. This should be.

myMethod()
  require(myMethid())
{
  /* */
}

==========
Native DbC support syntax:
class Child {
    require($this->age < 18); // Invariant (Class state condition)

    public function someMethod($input)
        require(somethingAbout($input)) // Precondition
        return($ret, somethingReturn($ret)) // Postcondition
    {
        /* Great! We are certain that caller satisfy precondition, return
           appropriate return value and have proper class state! */
    }
}

--
Yasuo Ohgaki
yohg...@ohgaki.net

Reply via email to