Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]
Groups > pl.comp.programming > #31562 > unrolled thread
| Started by | Maciej Sobczak <see.my.homepage@gmail.com> |
|---|---|
| First post | 2018-04-22 23:46 -0700 |
| Last post | 2018-05-05 12:45 -0700 |
| Articles | 5 — 4 participants |
Back to article view | Back to pl.comp.programming
Formal Methods Toolkit Maciej Sobczak <see.my.homepage@gmail.com> - 2018-04-22 23:46 -0700
Re: Formal Methods Toolkit denat 'POPIS/EU <NOSPAMtestowanije@go2.pl> - 2018-04-23 20:58 +0200
Re: Formal Methods Toolkit Roman Tyczka <noemail@because.no> - 2018-04-24 13:30 +0200
Re: Formal Methods Toolkit michal@kleczek.org - 2018-05-05 00:12 -0700
Re: Formal Methods Toolkit Maciej Sobczak <see.my.homepage@gmail.com> - 2018-05-05 12:45 -0700
| From | Maciej Sobczak <see.my.homepage@gmail.com> |
|---|---|
| Date | 2018-04-22 23:46 -0700 |
| Subject | Formal Methods Toolkit |
| Message-ID | <dd72cd71-0bb8-4b7e-ba81-97dace215a14@googlegroups.com> |
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
[toc] | [next] | [standalone]
| From | denat 'POPIS/EU <NOSPAMtestowanije@go2.pl> |
|---|---|
| Date | 2018-04-23 20:58 +0200 |
| Message-ID | <pblad3$v5n$2@node1.news.atman.pl> |
| In reply to | #31562 |
uwaga atak: rozpoznaje dźwięki?
[toc] | [prev] | [next] | [standalone]
| From | Roman Tyczka <noemail@because.no> |
|---|---|
| Date | 2018-04-24 13:30 +0200 |
| Message-ID | <dzlh4m71z56p$.dlg@tyczka.com> |
| In reply to | #31563 |
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
[toc] | [prev] | [next] | [standalone]
| From | michal@kleczek.org |
|---|---|
| Date | 2018-05-05 00:12 -0700 |
| Message-ID | <fd45a401-66fc-44da-b8d3-9ab4944da65a@googlegroups.com> |
| In reply to | #31562 |
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
[toc] | [prev] | [next] | [standalone]
| From | Maciej Sobczak <see.my.homepage@gmail.com> |
|---|---|
| Date | 2018-05-05 12:45 -0700 |
| Message-ID | <6ecc5bb5-2a4a-4a28-a5e3-f960676107fb@googlegroups.com> |
| In reply to | #31570 |
> 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
[toc] | [prev] | [standalone]
Back to top | Article view | pl.comp.programming
csiph-web