    Cursus   NWIIBC026  Categorie   BA (Bachelor)  Voertaal   Engels  Aangeboden door   Radboud Universiteit; Faculteit der Natuurwetenschappen, Wiskunde en Informatica; Informatica en Informatiekunde;  Docenten     Collegejaar   2022   Periode   KW3  (30012023 t/m 09042023) 
 Aanvangsblok   KW3  
 Onderwijsvorm   voltijd  
 Opmerking     Inschrijven via OSIRIS   Ja  Inschrijven voor bijvakkers   Ja  Voorinschrijving   Nee  Wachtlijst   Nee  Plaatsingsprocedure   Volgorde bepaald door opl./programma  Toelichting   Volgorde bepaald door opleiding/programma 
     
After this course participants are able to:
 Define the semantics of imperative language constructs using inductive methods.
 Explain the consequences of design choices.
 Analyze computations in imperative languages like termination behavior and semantic equivalence.
 Prove properties of programs using inference systems for correctness.
 Determine whether inference systems are sound and/or complete.


In this course, you will learn formalisms to define the operational semantics of imperative programming languages. These methods are important for designing new languages and extending existing languages. In addition, these formalisms are used for analyzing the behavior of programs. In the field of computing science, you will not only have to apply these formalisms, but you will also have to evaluate, expand or design these formalisms as well.
Instructional Modes
Typically, each week the course has three sessions:
 Plenary lectures. You are supposed to prepare for these lectures by doing a socalled preparation assignment. The first 2025 minutes of the lectures are used for answering your questions about these topics. The rest of the time is used for introducing the more complex topics. After the plenary lecture, the weekly learning task will be published.
 Parallel tutorial sessions. Within these sessions, you can work on the new learning task or ask questions about the previous task under the supervision of TAs.
 Response lectures. Within these sessions, solutions for selected exercises of the learning task are discussed. Note that you are only allowed to participate in these sessions if you handed in a serious attempt at a solution to the learning task.
Because most of the solutions to the exercises are not published, but only discussed in the response lectures, this course is not very well suited for selfstudy in the last few weeks. In fact, the experience from previous years shows that students who actively do the learning tasks every week, usually pass the course at the first opportunity.


 
You have programming experience with imperative programming languages. In addition, you are able to:
 use the language of predicate logic to formulate statements;
 distinguish the elementary steps within argumentation and present proofs in a suitable inference system;
 specify (programming) languages and extensions using regular expressions and contextfree grammars;
 formulate clearly, both in motivating solutions as well as in structured proofs in natural language.
You can obtain these prerequisites by doing the courses in the programming line, and by doing one of the courses IPC002 Languages and Automata or IPK001 Introduction to Formal Reasoning, and by doing the course IPI004 Logic and Applications. In addition, it helps if you have done the course IBC003 Computability, but that is not a formal requirement.


The course is finalized with a digital Cirrus exam.
By doing the weekly homework assignments properly, a small bonus can be earned. Note that enforced by the rules and regulations, the bonus can only be used to pass the course if the grade for the final exam is at least 5.0.

 


   Verplicht materiaalBoekHanne Riis Nielson and Flemming Nielson: Semantics with applications, 1999. The book is available for free as PDF via Brightspace. 
Titel  :   Semantics with applications 
Auteur  :   Hanne Riis Nielson and Flemming Nielson 
 DictaatEngelbert Hubbers: Annotated Programs, an alternative notation for correctness proofs. These notes are available as PDF via Brightspace. 
Titel  :   Annotated Programs 
Auteur  :   Engelbert Hubbers 


WerkvormenCourseAanwezigheidsplicht   Ja 
Opmerking84 hours.

 ToetsenDigital ExamWeging   1 
Toetsvorm   Digitale toets met CIRRUS 
Gelegenheden   Blok KW3, Blok KW4 
OpmerkingA small bonus can be earned with weekly assignments. The bonus is only valid if the grade for the exam is at least 5.0


  
 
 