Головна сторінка: Różnice pomiędzy wersjami
m (→Мапа) |
(Tłumaczenie 'Wizja przyszłości') |
||
| Linia 29: | Linia 29: | ||
|- | |- | ||
| − | |♥ LEM - це назва нового дослідницького проєкту. | + | |♥ ''LEM'' - це назва нового дослідницького проєкту. |
Метою цього проєкту є вивчення можливості створення мови програмування з певними визначеними характеристиками (див. [[специфікація LEM]]). | Метою цього проєкту є вивчення можливості створення мови програмування з певними визначеними характеристиками (див. [[специфікація LEM]]). | ||
Мова LEM має ґрунтуватися на досягненнях проекту Loglan'82 та використовувати найкращі аспекти об'єктно-орієнтованих мов програмування новіших поколінь: Java, C++, C#, Python і т.д.<br /> | Мова LEM має ґрунтуватися на досягненнях проекту Loglan'82 та використовувати найкращі аспекти об'єктно-орієнтованих мов програмування новіших поколінь: Java, C++, C#, Python і т.д.<br /> | ||
→ '''[[LЕM]]''' | → '''[[LЕM]]''' | ||
| − | |♥ Проєкт SpecVer має на меті підтвердити корисність застосування законів алгоритмічної логіки в інженерії програмного забезпечення. Мова LEM може виявитися корисною в роботі проєкту SpеcVer.<br /> | + | |♥ Проєкт ''SpecVer'' має на меті підтвердити корисність застосування законів алгоритмічної логіки в інженерії програмного забезпечення. Мова LEM може виявитися корисною в роботі проєкту SpеcVer.<br /> |
→ '''[[SpеcVer]]''' | → '''[[SpеcVer]]''' | ||
| + | |} | ||
| + | |||
| + | {| class="wikitable" | ||
| + | |- | ||
| + | |♥ Бібліотека класів і математичних знань, корисних для програмістів. <br /> | ||
| + | Візія майбутнього (ще один проєкт на роки роботи для багатьох людей). | ||
| + | |||
| + | Давайте почнемо з кількох питань: Чи можна вмістити математичні знання в комп'ютері? Чи можна вмістити інформатичні знання в комп'ютері? Дональд Кнут 70-х роках XX століття мав таку амбіцію, розпочинаючи створення своєї книги ''Мистецтво програмування''. Сьогодні, через майже 50 років, комп'ютерні знання зросли і здається неможливим, що їх можна вмістити в комп'ютері. Але, по-перше, комп'ютери тепер значно більші і швидші, ніж колись, а по-друге, існує комп'ютерна мережа (Здійснилася візія С. Лема з 50-х років). Це дозволяє нам перейти до створення ескізу концепції. <br /> | ||
| + | Необхідно було б : | ||
| + | # Створити сховище знань, якими користуються розробники програмного забезпечення. Тут будуть знаходитися бібліотеки класів і методів, а також знання про структури даних, в яких проводяться обчислення. Це стосується як структур реляційних (алгебраїчних), що розглядаються математиками, так і структур даних, визначених і використовуваних інженерами програмного забезпечення. | ||
| + | # Створити мову, якою розробники програмного забезпечення будуть писати свої аргументи для (друкованих, розповсюджуваних, ...) повідомлень. Така мова повинна бути зрозумілою для людей і достатньо формалізованою, щоб була можливість комп'ютерного аналізу передставлених доказів. | ||
| + | # Інструмент для перевірки достовірності доказів. Буде потрібна програма proof checker, який суттєво відрізнятиметься від Mizara та йому подібних, оскільки докази будуть записані в рахунку програм (тобто в системі AL), який багатший за рахунок предикатів. | ||
| + | # Придумати спосіб збирання та поширення знань. Чи це має бути щось на кшталт математично-алгоритмічної пошукової системи Google? | ||
|} | |} | ||
Wersja z 00:55, 5 mar 2024
Лотар Коллатц ( у 1937 році) мав рацію !
Карта
На цих сторінках ми представляємо чотири дослідницькі проєкти: Алгоритмічна логіка(з 1968), Loglan'82(з 1978), SpecVer(2007), Lem(2012).
Перші два проєкти дали багато результатів і будуть використовуватися ще багато років.
| ♥ Дослідницький проєкт "Алгоритмічна логіка" займається відкриттям законів рахунку програм і знаходить застосування у верифікації програм, тобто у доведенні істинності таких властивостей програм, як коректність, відсутність циклів тощо. Мова алгоритмічної логіки дозволяє не лише виражати властивості алгоритмів (програм), а й забезпечує аксіоматизацію багатьох структур даних. Це стосується як відомих і необхідних в алгоритміці структур даних (наприклад, стеки, бінарні дерева пошуку, купи і т. д.), так і багатьох структур, що вивчаються в математиці. Можна вважати, що математика займається дослідженням, чи є дана формула [math] \alpha [/math] істинною у даній структурі [math] \mathbb{A} [/math]. Однак більшість структур не можна описати за допомогою аксіом, записаних у логіці першого порядку! Прийняття мови алгоритмічної логіки (або коротше, алгоритмічної мови) дозволяє представити ... |
♥ Дослідницький проєкт "Loglan'82" сприяв створенню однойменної об'єктно-орієнтованої та розподіленої мови програмування. Публікація мови та розповсюдження компілятора передували дослідженням різних проблем.
Наведемо кілька прикладів: • Вирішення проблеми безпечного та ефективного вивільнення надлишкових об'єктів. |
| ♥ LEM - це назва нового дослідницького проєкту.
Метою цього проєкту є вивчення можливості створення мови програмування з певними визначеними характеристиками (див. специфікація LEM).
Мова LEM має ґрунтуватися на досягненнях проекту Loglan'82 та використовувати найкращі аспекти об'єктно-орієнтованих мов програмування новіших поколінь: Java, C++, C#, Python і т.д. |
♥ Проєкт SpecVer має на меті підтвердити корисність застосування законів алгоритмічної логіки в інженерії програмного забезпечення. Мова LEM може виявитися корисною в роботі проєкту SpеcVer. → SpеcVer |
♥ Бібліотека класів і математичних знань, корисних для програмістів. Візія майбутнього (ще один проєкт на роки роботи для багатьох людей). Давайте почнемо з кількох питань: Чи можна вмістити математичні знання в комп'ютері? Чи можна вмістити інформатичні знання в комп'ютері? Дональд Кнут 70-х роках XX століття мав таку амбіцію, розпочинаючи створення своєї книги Мистецтво програмування. Сьогодні, через майже 50 років, комп'ютерні знання зросли і здається неможливим, що їх можна вмістити в комп'ютері. Але, по-перше, комп'ютери тепер значно більші і швидші, ніж колись, а по-друге, існує комп'ютерна мережа (Здійснилася візія С. Лема з 50-х років). Це дозволяє нам перейти до створення ескізу концепції.
|
