FYI, в нова версия на сборника със задачи има алгоритъм за мода плюс доказателство за коректност с инварианта (стр. 113--117). Доказателството е суперподробно.  Естествено, не се очаква на контролно или изпит да има и 1/4 от това.

Алгоритъмът от примерните решения (на Георги) с вложените цикли, въпреки че има по-дълъг код, е по-лесен за верифициране.  Алгоритъмът със само един цикъл, каквито решения имаше, е по-тегав за формално верифициране, защото по същество той поддържа две различими състояния "текущият елемент от масива е равен на текущата мода" и неговата негацията, с възможно преминаване от първото във второто и от второто в първото.

Ако броячът за дължината на последния run не се инициализира извън цикъла, нещата стават още по-тегави, понеже стойността на тази променлива е недефинирана в началото и д-вото на инвариантата би искало две отделни бази, за да бъде всичко формално изпипано.  Това е обяснено надълго в сборника.

--

ММ

Last modified: Tuesday, 6 May 2014, 9:55 PM