Z przyjemnością informuję o dostępności nowego narzędzia:

http://inspirel.com/fmt/

FMT jest pakietem rozszerzeń dla programu Mathematica, pozwalającym na tworzenie
modeli, analizę, wizualizaję, weryfikację i generację kodu dla Ady, C i C++.

Kilka zrzutów ekranu pokazuje próbkę możliwości:

http://inspirel.com/fmt/gallery.html

FMT jest narzędziem open-source.


Chętnie odpowiem na pytania.

--
Maciej Sobczak * http://www.inspirel.com

do góry

uwaga atak:
rozpoznaje dźwięki?

do góry

On Mon, 23 Apr 2018 20:58:41 +0200, denat 'POPIS/EU wrote:

> uwaga atak:
> rozpoznaje dźwięki?

https://www.youtube.com/watch?v=j9ejj_fD-P0

--
pozdrawiam
Roman Tyczka

do góry

On Monday, April 23, 2018 at 7:46:23 AM UTC+1, Maciej Sobczak wrote:
> Z przyjemnością informuję o dostępności nowego narzędzia:
>
> http://inspirel.com/fmt/
>
> FMT jest pakietem rozszerzeń dla programu Mathematica, pozwalającym na tworzenie
modeli, analizę, wizualizaję, weryfikację i generację kodu dla Ady, C i C++.
>
> Kilka zrzutów ekranu pokazuje próbkę możliwości:
>
> http://inspirel.com/fmt/gallery.html
>
> FMT jest narzędziem open-source.
>
>
> Chętnie odpowiem na pytania.
>

Czy to jest po prostu nowy język programowania pozwalający na jakąś formę dowodzenia
poprawności?
Jak on się ma do - coraz popularniejszych, choć wciąż niszowych - języków typu Coq,
Agda, Idris opartych o dependent types?

--
Michal

do góry

> 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

do góry