История изменений

Вообще то, насколько я понял, теория массивов это часть математической логики позволяющая доказать средствами математической логики что алгоритм с массивом делает ровно то, что нужно. Вещь как мне кажется в себе - в тривиальных случаях пустая трата времени, в нетривиальных этой темой никто толком не владеет на нужном уровне для практического использования. М.б. есть какие то статические анализаторы кода где это юзается, я ХЗ.

SMT же вообще прекрасная как сферический конь в вакууме. Если SAT сейчас вовсю используют при разных оптимизациях (хотя свести практическую задачу к SAT тот еще гемор), то про успехи SMT я особо не слышал. Ну то есть где то может взлететь, но в общем виде оно чересчур сложное.

Вообще то, насколько я понял, теория массивов это часть математической логики позволяющая доказать средствами математической логики что алгоритм делает ровно то, что нужно. Вещь как мне кажется в себе - в тривиальных случаях пустая трата времени, в нетривиальных этой темой никто толком не владеет на нужном уровне для практического использования. М.б. есть какие то статические анализаторы кода где это юзается, я ХЗ.

SMT же вообще прекрасная как сферический конь в вакууме. Если SAT сейчас вовсю используют при разных оптимизациях (хотя свести практическую задачу к SAT тот еще гемор), то про успехи SMT я особо не слышал. Ну то есть где то может взлететь, но в общем виде оно чересчур сложное.