-
Data: 2018-05-05 21:45:05
Temat: Re: Formal Methods Toolkit
Od: Maciej Sobczak <s...@g...com> szukaj wiadomości tego autora
[ pokaż wszystkie nagłówki ]> Czy to jest po prostu nowy język programowania
Sprawa jest bardziej złożona. Nie jest to zupełnie nowy język, bo wykorzystuje
gramatykę języka Wolfram. Tzn. każda konstrukcja w FMT jest poprawnym wyrażeniem
języka Wolfram, choć z nowym znaczeniem wynikającym z tego, jak dane wyrażenie jest
dalej obrabiane. Nie jest to też po prostu język programowania, bo nacisk jest na
modelowanie systemu na poziomie wymagań niskopoziomowych. W swoim rdzeniu taki model
faktycznie wygląda jak imperatywny kod albo pseudokod, ale nie jest to ograniczenie i
być może język zostanie rozwinięty w stronę bardziej wysokopoziomowych konstrukcji,
niekoniecznie opartych na kodzie w sensie tekstowego formatu. Ostatecznie kod
programu jest generowany na podstawie modelu.
> pozwalający na jakąś formę dowodzenia poprawności?
Tak, ideą jest statyczne dowodzenie różnych wybranych cech modelu.
> Jak on się ma do - coraz popularniejszych, choć wciąż niszowych - języków typu Coq,
Agda, Idris opartych o dependent types?
1. Podstawowym założeniem w FMT jest zdolność do wygenerowania kodu, który w ogóle
nie potrzebuje run-time'u, co ma ułatwić wdrożenie w *prawdziwych* systemach
krytycznych, czyli takich, które podlegają narzuconym z góry przemysłowym standardom.
Czyli żadnej pamięci dynamicznej (nawet niejawnej), itp. Celem jest też generacja
kodu w Adzie lub w C(++), które są standardowymi językami wykorzystywanymi w
przemyśle - po to, żeby można było taki wygenerowany kod użyć w jakimś regularnym i
uznanym obecnie procesie produkcyjnym. Inaczej mówiąc, można użyć FMT w obecnym
procesie, bez technicznych rewolucji, bo z punktu widzenia obecnych procesów jest to
tzw. Model-Based Design z generatorem kodu, czyli coś, co z powodzeniem uprawia się
od dawna (patrz np. Simulink, SCADE, itp.).
O ile zgaduję, takie założenia nie były priorytetem w tych językach, które
wymieniłeś.
2. Co to jest "dependent types"?
W FMT system typów to ścisły podzbiór tego, co można osiągnąć w C albo w Adzie. Ma to
związek z założeniami powyżej.
--
Maciej Sobczak * http://www.inspirel.com
Najnowsze wątki z tej grupy
- Bibl. Qt jest sztucznie ograniczona - jest nieprzydatna do celów komercyjnych
- Co sciaga kretynow
- AEiC 2024 - Ada-Europe conference - Deadlines Approaching
- Jakie są dobre zasady programowania programów opartych na wtyczkach?
- sprawdzanie słów kluczowych dot. zła
- Re: W czym sie teraz pisze programy??
- Re: (PDF) Surgical Pathology of Non-neoplastic Gastrointestinal Diseases by Lizhi Zhang
- CfC 28th Ada-Europe Int. Conf. Reliable Software Technologies
- Młodzi programiści i tajna policja
- Ada 2022 Language Reference Manual to be Published by Springer
- Press Release - AEiC 2023, Ada-Europe Reliable Softw. Technol.
- Ada-Europe - AEiC 2023 early registration deadline approaching
- Ada-Europe Int.Conf. Reliable Software Technologies, AEiC 2023
- Ile cykli zajmuje mnożenie liczb 64-bitowych?
- Ideologia Polskiego Programisty wer.3
Najnowsze wątki
- 2024-04-27 Nowy, "szybki "komputer AsRock nie posiada modułu TPM
- 2024-04-27 Nowy, "szybki "komputer AsRock nie posiada modułu TPM
- 2024-04-27 Warszawa => Inżynier DevOps (projekt JP) <=
- 2024-04-27 Warszawa => Senior Account Manager (on-site) <=
- 2024-04-27 Wrocław => Dyrektor Sprzedaży (branża usług/produktów IT) <=
- 2024-04-27 Warszawa => Sales Representative for Outsourcing Services <=
- 2024-04-27 Chrzanów => Administrator i wdrożeniowiec Lotus Notes/Domino <=
- 2024-04-27 Ja pierdolę...
- 2024-04-27 Ryby i kawitacja
- 2024-04-27 Zabrze => Junior HelpDesk <=
- 2024-04-27 Katowice => Administrator IT - Wirtualizacja i Konteneryzacja <=
- 2024-04-27 Bażanowice => Inżynier Industrializacji - Elektronik <=
- 2024-04-27 Warszawa => Full Stack web developer (obszar .Net Core, Angular6+) <=
- 2024-04-27 Zadaszenie tarasu, a wymagany spadek
- 2024-04-27 Warszawa => Senior Account Manager <=