FMSE
Formal
Methods in
Software Engineering
Pages CS2105O2 Principii ale limbajelor de ... Anonymous  Login

CS2105O2 Principii ale limbajelor de programare

 Incepand cu anul universitar 2015-2016, cursul are un nou sit: http://sites.google.com/site/fiicourseplp/

Observatie. Acesta este planul initial al cursului, e posibil ca pe parcurs sa apara modificari. 

 

Cursuri

Partea I Introducere

Curs 1 Despre limbajele de programare

KFramework (instalare, utilizare)

Curs 2 Sintaxa limbajelor de programare.

Sintaxa limbajului IMP. 

Resurse biliografice: K Tutorial, IMP, Lesson 1

Curs 3 Semantica operationala a unui limbaj imperativ simplu

Semantica limbajului IMP. 

Resurse biliografice: K Tutorial, IMP, Lesson 2,3,4, 5

 

Partea II Definirea unui limbaj real (CinK)

 

Curs 4 Concepte de baza 

     Implementarea lui int: int.k   Testul pentru int: test-int.zip

    Exercitii: sa se implementeze celelalte tipuri intregi din C++

Curs 5 Expresii - Sintaxa 

   Implementarea k Teste

   Exercitiu: sa se adauge sintaxa operatorilor aritmetici C++ care lipsesc.

Curs 6 Expresii  Semantica 

   Implementarea K

    Exercitiu: sa se dea semantica operatorilor adaugati la lectia anterioara.

Curs 7 Instructiuni

  Implementarea K

   Exrcitiu. 1. Sa se dea semantica instructiunii bloc salvand "environment"-ul local intr-o celula separata (<bstack>), ce va fi organizata ca stiva. Salvarea nu se va face decat daca environment-ul curent este diferit de cel din varful stivei.

  2. Sa se dea semantica la celelalte instructiuni de selectie si repetitive. Se va da bonus pentru instructiunile de salt.

Curs 8 Pointeri, referinte, tablouri

Implementarea K (lesson5.zip)

   Exercitiu: 1. Sa se scrie mai multe xemple de programe si sa testeze semantica tabourilor.

2. Sa se adauge initializarea de tablouri.

3. Sa se modifice semnatica tablourilor astfel incat sa verifice depasirea intrevalelor pentru indici.

 

Curs 8,9 Functii

Implementarea K (lesson6.zip)

 Prezentarea

Exercitii. 1. Cum se modifica semantica pentru cazul cand exista functii supraincarcate.

2. Sa se adauge functionalitatea data de valorile implicite ale parametrilor.

 

Partea a III-a Definirea unui limbaj functional simplu (FUN)

  Prezentare

  Posterul pdf pentru FUN

  Definitia lui FUN se gaseste in k/tutorial/2_languages/3_fun/1_untyped/.

Partea a IV-a Analiza de programe

 

Verificare

40% testul scris (sapt 15,16)

   Exemple de exercitii pentru testul scris.

60% laborator

  • 10 puncte instalarea si familiarizarea cu frameworkul K
  • 20 puncte extensia lui IMP
  • 30 puncte extensiile la Cink

 Test 30.01.2015

1. Nu este permisa utilizarea bibliografiei. Se permite totusi o foaie A4 cu definitia IMPului. Foaia va fi atasata la test.

Barem:

1. 3p arborele de parsare pentru a), 3p) motivatie ce b) nu face parte din limbaj, 4p arborele sintactic abstract, 2p observarea ambiguitatii

2. 4 puncte aplicarea regulilor de "heating/cooling" generetate din adnotarile sintaxei, 4p aplicarea regulilor scrise explicit in sintaxa, 4p descrierea corecta a calculului

3. 2p descriere ce este un pointer (o variabila a carei valori sunt adrese ale altor obiecte din memorie), 4p declarare, 3p operatorul *, 3p operatorul &.

Rezultatele la testul din 30.01 si laborator.

Cine are minim 45 puncte a promovat. Eventualele observatii pot fi trimise prin email pana pe 31.01.2015 ora 12.

Test 13.02.2015

Rezultatele (baremul de promivare a fost scazut la 40).

Fisa disciplinei 

Bibliografie

K Tutorial

Traian Florin Serbanuta and Andrei Arusoaie and David Lazar and Chucky Ellison and Dorel Lucanu and Grigore Rosu. The K Primer (version 3.3) 

Dorel Lucanu, Traian Serbanuta. CinK - an exercise on how to think in K TR 12-03, Version 2, Alexandru Ioan Cuza University, Faculty of Computer Science, 2013

ISO C++ standard. Working draft

Highlighting definition for Notepad++.

Laboratoare

Laborator 1: Instalare K, familiarizare cu framework-ul

Laborator 2: Experimente cu sintaxa IMP-ului

Laborator 3: Experimente cu semantica IMP-ului

Exercitii:

  1. Extindeti definitia IMPului cu
  • operatori aritmetici si booleeni (similar ca in C++, operatori fara "side-effect")
  • instructiunile for, do-while, switch (similar ca in C++)
  • variabile booleene.
  • (Bonus) instructiunile break, continue, goto,

 Laborator 4: Experimente cu functii / expresii cu side-effects

 Exercitii:

  1. Extindeti Cink-lesson1 cu tipurile unsigned int, long int, unsigned long int (sec. 2.14.2 din manualul de C++).

 Laborator 5: Expresii II

 Laborator 6: Arrays, Pointers



NEWS
New publication : Model checking recursive programs interacting via ... - 01 feb 2015

Almost all modern imperative programming languages include operations for dynamically manipulating the heap, for example by allocating and deallocating objects, and by updating reference fields. In the presence of recursive ... (more)


New publication : K-Java: A Complete Semantics of Java - 10 sep 2014

This paper presents K-Java, a complete executable formal semantics of Java 1.4.
K-Java was extensively tested with a test suite developed alongside the project, following the Test Driven Development methodology.
more)


New publication : K-Java: A Complete Semantics of Java - 09 jul 2014

This paper presents K-Java, a complete executable formal semantics of Java 1.4.
K-Java was extensively tested with a test suite developed alongside the project, following the Test Driven Development methodology.
more)


New publication : Engineering Hoare Logic-based Program Verification in ... - 30 oct 2013

We propose a language-independent symbolic execution framework for languages endowed with a formal operational semantics based on term rewriting. Starting from a given definition of a language, a new language ... (more)


New talk: PAS 2013 - 20 oct 2013

Dorel lucanu will give a talk at PAS 2013.

(more)

     Archive

@FMSE 2010-2011