_                       __
                      o                    | |  o                  /  \
          __   __        __,     ,_    __  | |      _    _|_         _/
         /    /  \_   | /  |    /  |  /  \_|/ \_|  |/     |  |   |  |
         \___/\__/    |/\_/|_/     |_/\__/  \_/ |_/|__/   |_/ \_/|_/o
                     /|                              \_
                     \|

                              8.XI.2010

                  ___                     __
                   |  _  _| _     _ _    (_  _ __     |
                   | (_|(_|(/_|_|_> /_   __) /_| ||_| |<







================================================================================

Plan prezentacji
=================

  * KrĂłtka historia BML-a.

  * Problemy z BML-em.

  * Pomysł na nowy standard specyfikacji bajtkodu. 

  * Dalsze plany.













================================================================================

KrĂłtka historia BML-a.
=======================

  * Stworzony w ramach MOBIUS-a.

  * Podstawowe przeznaczenie: PCC.

  * Jest to w zasadzie JML zapakowany w plik .class.

  * Zestaw narzędzi:
      
     - BMLLib: podstawowa biblioteka.

     - Umbra: edytor
     
     - JML2BML - translator z JML.

     - BMLVCGEN, BML2BPL - VCGen-y.

  * Case study: Bill 



================================================================================

Klasa Bill
===========

  * Zawiera dwie metody (jedna jest abstrakcyjna), 
    pętlę z niezmiennikiem oraz niezmiennik klasowy.

  * Próby weryfikacji za pomocą zestawu BML-owych narzędzi 
    przyniosły następujące rezultaty:

     - Podstawową biblioteka i pozostałe narzędzia wymagały 
       licznych przerĂłbek.
     
     - VCGen wygenerował dużą ilość formuł coq-owych
         :: Niestety nie do końca właściwych.
         :: Złożoność formuł powstających w trakcie dowodu
            często prowadziła do zawieszania się systemu. 
     
     - Ostatecznie dowód powstał kosztem wielu dni pracy.         

     - Zweryfikowanie jakiegokolwiek systemu o praktycznych 
       rozmiarach jest ta metodą niemożliwe.


================================================================================

Wady dotychczasowego podejścia
===============================

  * Brak jakiegokolwiek wsparcia dla automatycznej weryfikacji.

  * Przekomplikowane i słabo działające narzędzia.

  * BML jest kiepsko przystosowany do opisu bajtkodu.

     - Jest zbyt silnie związany z JML.

     - Tworzenie narzędzi przetwarzających BML jest trudne. 

     - Mechanizm konstrukcji dowodu polegający na użyciu Bicolano 
       oraz wielu zapisanych w Coq-u przkształceń jest nieefektywny 
       i tworzy mało przejrzyste formuły.

  * Wiele bardziej zaawansowanych kwestii związanych z generowaniem
    obligacji dowodowych zostało zignorowanych podczas projektowania
    języka specyfikacji.



================================================================================

Wnioski
========

  * Weryfikacja bez wsparcia ze strony automatycznych solverĂłw
    jest zbyt złożona nawet dla małych programów.

     - Zwłaszcza po uwzględnieniu niskopoziomowego charakteru bajtkodu.

  * Bajtkod potrzebuje innego języka weryfikacji niż Java.

  * Potrzebna jest duża liczba różnych narzędzi.

  * Trzebaby tego Bill-a zrobić na poważnie.




                          "But there's no sense crying over every mistake.
                           You just keep on trying till you run out of cake."
                                                                   



================================================================================



        ____                            __      __
       /\  _`\               __        /\ \    /\ \__
       \ \ \L\ \_ __   ___  /\_\     __\ \ \/'\\ \ ,_\
        \ \ ,__/\`'__\/ __`\\/\ \  /'__`\ \ , < \ \ \/
         \ \ \/\ \ \//\ \L\ \\ \ \/\  __/\ \ \\`\\ \ \_
          \ \_\ \ \_\\ \____/_\ \ \ \____\\ \_\ \_\ \__\
           \/_/  \/_/ \/___//\ \_\ \/____/ \/_/\/_/\/__/
                            \ \____/
                             \/___/

       __      __  ______   __       __     ______   ______
      /\ \  __/\ \/\__  _\ /\ \     /\ \   /\__  _\ /\  _  \  /'\_/`\
      \ \ \/\ \ \ \/_/\ \/ \ \ \    \ \ \  \/_/\ \/ \ \ \L\ \/\      \
       \ \ \ \ \ \ \ \ \ \  \ \ \  __\ \ \  __\ \ \  \ \  __ \ \ \__\ \
        \ \ \_/ \_\ \ \_\ \__\ \ \L\ \\ \ \L\ \\_\ \__\ \ \/\ \ \ \_/\ \
         \ `\___x___/ /\_____\\ \____/ \ \____//\_____\\ \_\ \_\ \_\\ \_\
          '\/__//__/  \/_____/ \/___/   \/___/ \/_____/ \/_/\/_/\/_/ \/_/




================================================================================

Założenia
==========

  * Nowy język specyfikacji dla bajtkodu.

  * NIE będący przeróbką JML.

  * Łatwy w implementacji.

  * Kilka implementacji zamiast jednej biblioteki.

  * Weryfikacja zautomatyzowana.

  * Język NIE musi być czytelny.

  * Bez zamiatania pod dywan (aliasowania, refleksja, 
                              wielowątkowość, finalizacja).

  * Język wyrażeń = bajtkod.

  * Zestaw narzędzi do Eclipse.


================================================================================

Po co nowy język?
==================

  * Stary się nie sprawdził.

  * Nie jest łatwo go naprawić.

      - Stan implementacji temu nie sprzyja.

      - Niektóre decyzje projektowe należałoby zmienić.

  * JML ma sporo wad, z którymi można się przy okazji zmierzyć.

  * Oczywiście ciężko byłoby zmienić JML...

      - Ale BML ma znacznie słabszą pozycję.







================================================================================

Czemu nie oprzeć się na JML?
=============================

  * Bo łatwo się wtedy przewrócić.

  * JML korzysta z wyrażeń Javowych. W efekcie każde narzędzie
    musiałoby rozumieć dwa różne języki wyrażeń - JML i bajtkod.

  * JML średnio sobie radzi z kontrolą aliasowania, refleksją itp.

  * JML ma nieco inne przeznaczenie - powinien być czytelny
    i bezpośrednio zapisywalny przez programistę.

  * Dla języków innych niż Java korzystanie z języka specyfikacji
    opartego na JML może być niewygodne.

  * JML jest olbrzymim standardem, do którego doklejane są wciąż
    nowe koncepcje. W efekcie żadne narzędzie nie 'rozumie' 
    całego JML.




================================================================================

Po co kilka implementacji?
===========================

  * Mamy wiele róşnych bibliotek do bajtkodu.

      - BCEL

      - ASM

      - SAWJA

      - ...

  * Przy projektowaniu narzędzia wybór bywa ograniczony.

      - Czasem istniejące narzędzie używa już ktorejś biblioteki 
        i nie jest łatwo to zmienić. 

  * Pozwoli to zweryfikować założenie o prostocie języka.



  
================================================================================

Czytelność
===========

  * Bajtkod nie jest czytelny.

  * I nie musi, bo przecież nikt go bezpośrednio nie pisze.

  * Więc język specyfikacji mógłby mieć podobne własności.

  * Czasem jednak dobrze byłoby móc przeczytać specyfikację
    biblioteki, z której się korzysta.

  * Można wtedy użyć źródłowej postaci tejże specyfikacji,
    udostępnianej na zasadach podobnych jak symbole
    do odpluskwiania.

  * Oczywiście nieczytelność sama w sobie nie jest zaletą,
    ale usunięcie z języka wszelkich postaci lukru 
    syntaktycznego (czyli zapewnienie jego prostoty przy
    zachowaniu siły wyrazu) w naturalny sposób do niej
    prowadzi.


================================================================================

Implementacja
==============

  * Można założyć, że implementacja biblioteki obsługującej
    nasz nowy język będzie korzystać z jednej z bibliotek
    bajtkodowych.

  * Byłoby dobrze, gdyby nie było potrzeba wiele więcej.

  * Więc można użyć bajtkodu do opisu formuł i wyrażeń.

  * Oczywiście są pewne problemy np. z kwantyfikatorami.

  * Żeby przeciętna biblioteka mogła sparsować ww. wyrażenia,
    trzeba je zapakować w treści metod, a nie na przykład
    atrybuty (jak BML) czy adnotacje (JIR).

  * Wynik takiego działania jest dość paskudny i niskopoziomowy,
    ale za to łatwy do uzyskania i przetwarzania.




================================================================================

Specyfikacje w Javie
=====================

  * Specyfikacje w bajtkodzie będą skompilowaną wersją 
    specyfikacji w innych językach.

  * W szczególności JML.
    
  * Na razie jednak trzeba je bęzie pisać ręcznie.
    
  * Edytowanie bajtkodu jest niezbyt przyjemne.
  
  * Można jednak tak zaprojektować język specyfikacji,
    żeby dało się uzyskać stosowny plik pisząc w samej Javie/
    
      - Wszelkie metainformacje kodowane w adnotacjach, 
        a nie na przykład atrybutach.
        
      - Każdy kawałek bajtkodu musi być w treści jakiejś metody.
      


      
================================================================================

Dywan
======

  * Opisywany język ma pełnić rolę kodu pośredniego 
    dla innycn języków specyfikacji.
    
  * Więc w szczegolności nie może pomijać zagadnień, 
    które we wspomnianych językach są obsługiwane.
    
  * Tradycja formalnej specyfikacji każe zamieść pod dywan:
      - Wielowątkowość
      - Refleksję
      - Finalizację
      - ...
      
  * Jak je wymieść spod ww. dywanu?
      - Odsłaniając struktury danych maszyny wirtualnej
      - Używając dynamicznych ramek
      - Dwustanowych niemziennikĂłw
      - ???                              <------

  

================================================================================
  
Eclipse
========

  * Projekt tego typu i rozmiaru jest umiarkowanie sensowny,
    jeśli nikt nie będzie z niego potem korzystał.

  * Trzeba go więc sprzedać.

  * W tym celu musi być kolorowy.

  * Eclipse pozwoli spełnić to wymaganie.

  * Ponadto pewne narzędzia zawarte w Eclipse, w szczególności
    EMF oraz Xtext, mogą być bardzo przydatne przy pierwszej
    implementacji nowego języka.

  * Spora grupa ludzi, którzy mogą być zainteresowani omawianym
    projektem, ma doświadczenie w tworzeniu wtyczek do Eclipse.





================================================================================

Narzędzia
==========

  * VCGen korzystający z Boogie.
  
  * Edytor bajtkodu i specyfikacji.
  
  * Tłumaczenie z JML.
  
  * Specyfikacje dla innych języków używających JVM.
  
     - Scala?
     
  * Integracja z Eclipsowymi narzędziami do JML?
  
  * Abstrakcyjna interpretacja bajtkodu?
  
  * Sporo pomniejszych programĂłw.
  

  
  

==============================================================================

Dalsze plany
=============

  * Bajtkod jest w zasadzie wysokopoziomowy. 
  
  * W przypadku PCC jest to wada.
  
  * Można więc próbować zejść trochę niżej:
  
     - Bajtkod LLVM
     - Instrukcje prostego mikrokontrolera (np. AVR).

  * Skoro usuwamy refleksję spod dywanu, to może przy okazji
    sprobować zastosować specyfikacje w językach dynamicznie 
    typowanych?
    
      - Na przykład w języku Lua.
      
      - NIE w Pythonie.
      
      - Ani tym bardziej tym czymś na 'R'.

      
==============================================================================