[nem-pl] z cyklu oglądamy i krytykujemy

[olszta at tey.pl]

Ja to jeszcze powolutku przemysle, ale...

Mamy trzy rodzaje asercji: zwykle eiffelowe, straznikow dla zmiennych
i straznikow dla blokow. Dodatkowo dodajemy pojecie transakcji, w czasie
jej wykonywania obudzeni straznicy odkladani sa na stos i uruchamiani
po jej zakonczeniu. Oprocz tego dodajemy atrybut pure dla funkcji, ktory
oznacza ze funkcja nie ma efektow ubocznych (modulo allokacja pamieci).
I na dokladke slowa kluczowe: value i previous.

Wyglada to tak:

0) definiujemy atrybut pure 

Da sie to latwo sprawdzic, jesli czasami bedziemy mogli sklamac.

1) warunek poczatkowy dla bloku wykonywalnego:

require { [warunek]; [warunek]; ... }

Gdzie [warunek]; to cokolwiek pure, co ewaluuje sie do boola.
Warunki sa sprawdzane w momencie wejscia do bloku.

2) warunek koncowy dla bloku wykonywalnego:

ensure { [warunek]; [warunek]; ... }

Podobnie jak wyzej, ale sprawdzane w momencie wyjscia z bloku,
dodatkowo mozliwosc skorzystania ze slowa kluczowego value, ktore
oznacza wartosc zwracana z danego bloku.

3) straznik dla bloku wykonywalnego:

guard { [warunek]; [warunek]; ... }

To sa niezmienniki na poziomie calego bloku, podobnie jak require,
ale sprawdzane po kazdej instrukcji w bloku, a nie tylko na jego
koncu (tu oczywiscie mozliwe sa pewne optymalizacje, ale to nie
jest istotne w tej chwili).

Tutaj jest taki problem, ze to jest bardzo fajne, jesli mamy
zdefiniowane petle w jezyku (np. while). Inaczej przydaje sie to
tylko w bardzo prostych programach.

4) straznik dla zmiennej:

guarded [nazwa zmiennej] : [typ]
{
  [warunek]; [warunek]; ...
}

Takie zmienne mozna definiowac zarowno w klasach, jak i w funkcjach
i zachowuja sie one dokladnie, jak zmienne mutable.

Przy kazdej probie zapisu do takiej zmiennej, sa sprawdzane warunki.

Mozna skorzystan z kwalifikatora previous (np. previous.x) aby uzyskac
dostep do poprzedniej wartosci zmiennej.

Trzeba dokladnie przemyslec, kiedy zaczac uruchamiac straznikow
(np. nie w czasie konstrukcji), ew. zwalic to na transaction.

5) straznik dla klas i wariantow

Syntaktycznie podobnie jak 3), ale dotyczy pol i funkcji klasy lub
wariantu.

-- PRZYKLAD --------------------

class Factorial
{
  guard
  {
    _n * _accumulator < System.Int32.MaxInt;
  }

  public guarded _n : int
  {
     _n >= 0;
     previous._n > _n;
  }

  public guarded _accumulator : int
  {
     _accumulator >= 1; 
     previous._accumulator < _accumulator;
  }

  public Step () : void
  {
    require { _n > 1; }

    transaction
    {
      _accumulator *= _n;
      _n--;
    }
  }

  public PerformSteps () : void
  {    
    if (_n > 1) { Step(); PerformSteps(); }
  }

  public CalculateFactorial (n : int) : int
  {
    transaction
    {
      _n = n;
      _accumulator = 1;
    }

    PerformSteps ();

    _n;

    ensure { _n > 0; }
  }
}