Привіт!
Нічого в цьому не розумію, тому дуже цікаво було почитати саме практичну статтю без глибокого занурення в теорію і математику.
Можете, будь ласка, трішки детальніше пояснити наступне: 1. Confusion matrix — як її правильно інтерпретувати?
Пишіть українською — це наша ідентичність. DOU приймає статті тільки українською — і це не просто правило редакції, а вибір спільноти. 73% топових статей уже українською, тренд зростає. Люди свідомо пишуть рідною, відправляючи в забуття мову агресора.
Це не складно до речі, DOU вже все зробив по факту, але з тегами кажись перебір, їх треба категоризувати мабуть, потім робити рубрікатор на основі них.
це занадто складно
незважаючи що це складова програмування на «лопаті»)
usigned overflow це визначена операція, тому ніяких проблем немає
так, якщо тільки з точки зору UB, різниця uint int є
спеціально зроблений максимально примітивно
я би сказав що то занадто, бо значно погіршує читабельність і вносить додаткові місця де помилитися можливо — тобто як приклад якраз краще і не надавати (imho)
Макрос N_ELEMENTS взагалі нуль змін
Тобто...
Класний проект. Підтримую що то робота профільних державних інституцій підтримувати таке. Особливо дякую за просте та конкретне пояснення як це відбувалось.
Та це просто навчальний приклад, спеціально зроблений максимально примітивно, щоб не навантажувати читача. Макрос N_ELEMENTS взагалі нуль змін в доказах.
Так, корисно/цікаво ознайомитись, особливо якщо не часто стикаєшся з тим, і викладено нормально. Питання не по самій верифікації, а по прикладу — на сі вже так наврядчи хто пише, то пов’язано з обмеженнями самого софта CoQ?
Ок, треба підправити, додати пояснення Просто англійська, там abs та mod...
Аглебраїчні структури так, але тут скоріше переход з однієї структури на іншу, так зазвичай комутативні диаграми читають.
Коментарі