Skip to content

Latest commit

 

History

History
125 lines (79 loc) · 3.48 KB

stress24-logika-schedule-instructor.md

File metadata and controls

125 lines (79 loc) · 3.48 KB
Raw

stress24

This file contains instructor notes for the STRESS 2024 lectures on Logika

Schedule

M1 (John)

Slang Overview (10 mins)

  • Slang purpose and design goals
  • Slang use (implemenenting Sireum, HAMR context)
  • Slang language features (example based)
  • Pointers to more information

Logika Overview (10 mins - 20 mins total)

  • Logika purpose and design goals
  • Logika use (Slang stand alone, HAMR context)
  • Logika GUI illustration
  • Logika scalability
  • Contract example (just viewing)
  • Deduce examples (just viewing)
  • Advanced manual proof with rewriting examples (just viewing)
  • Teaching material

Logika UI Principles -- Interactive (15 mins - 35 minutes total)

  • idea:
    • students click around on bolts and bulbs in various examples, they seed various errors and show them being detected, etc.
    • this could be based on the Waypoint Example. Note, if this is converted to Presentasi, then it could be broken into three sections

Logika Checking for Conditional Statements (15 mins - 50 minutes total)

Logika Checking for Compositional Reasoning (15 mins - 1:05 minutes total)

  • idea:
    • students are given partial program and the goal is to add method implementation, method clients, and contracts to illustrate compositional reasoning
    • guided exercise

Features Overview

  • datatypes / records
  • ???
  • point them to folder of examples

Extended exercise

  • idea:
    • students are given a description of code and specifications to write, potentially along with some starting content
    • possible example:
      • parts of Stefan's fibonacci example
      • max3 directly, and max3 in terms of max2
    • slang/logika features
      • conditionals
      • contracts
      • method calls
    • pitfalls: need to make sure that students have enough documentation.
  • What example should be used for this?

M2 (Stefan)

Solution walkthrough of exercise given before break (5 mins) (John)

Logika Checking for Loops, Loop Invariants -- Interactive -- Stefan (15 mins)

  • idea:
    • students are presented with loops for integer calculations (summing, factorial)

Logika Checking for Sequences, Quantification -- Interactive -- Stefan (15 mins)

  • idea:
    • students are presented with examples of sequences, quantification, index bounds checking, etc.
    • consider example to find max or min element in a sequence (as needed for insertion sort)

Extended exercise - Stefan (25 mins)

  • idea:
    • students are given a description of code and specifications to write, potentially along with some starting content
    • if we give the students the code for selection sort (as built up in previous activties, they could be asked to do bubble sort)
    • slang/logika features
      • loops, sequences, quantification
  • What example should be used for this?

Possible progression

  • findMin - sequences, quantification
  • swap - mutable
  • selection sort ==>
  • bubble sort

A1

Manual Proofs / Rewriting Overview -- John or Stefan

  • idea:
    • students are given completed examples of rewriting, etc.
    • slang/logika features
      • rewriting, rules
  • What example should be used for this?

???

Extended exercise

Other Verificaton Concepts Supported in Logika (?? where exactly would this go ??)

  • in the logika example of conformance-swap, there is a proof of equivalence between swapping by arithemetic and swapping by updates

A2

HAMR / GUMBO Overview -- John

Extended exercise (based on Isolette)