Задача по семантика на езиците за програмиране

[didetyyy_92]

Здравейте! Имам нужда от помощ за следната задача:

Като се използва аксиоматичният подход да се синтезира подпрограма-метод, която да провери колко от елементите на масива a[0:n-1], където n>0, са 0.Масивът е разреден, ако повечето му елементи са 0.Да се изведат елементите на масива а и да се провери дали е разреден. Синтезираната PDL програма да се трансформира първо в Spec# програма,а след това в C# windows приложение.

Благодаря предварително.