Cookies disclaimer

I agree Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.

Exercise 4 (Abstract Interpreter)

This is the task corresponding to exercise 4.


Download Files

Definitions File

theory Defs imports Complex_Main begin

no_notation less_eq  ("(_/ \<le> _)"  [51, 51] 50)

type_synonym vname = string

datatype aexp = N int | R rat | V vname | Plus aexp aexp

datatype Num = S | I | F | R


Template File

theory Submission imports Defs begin   

definition less_num :: "Num \<Rightarrow> Num \<Rightarrow> bool" ("(_/ \<le> _)"  [51, 51] 50) where
  "x \<le> y = undefined"

definition sup_num :: "Num \<Rightarrow> Num \<Rightarrow> Num" ("(_/ \<squnion> _)" [51, 51] 50) where
  "x \<squnion> y = undefined"

fun plus' :: "Num \<Rightarrow> Num \<Rightarrow> Num" where
  "plus' _ _ = undefined"

fun mul' :: "Num \<Rightarrow> Num \<Rightarrow> Num" where
  "mul' _ _ = undefined"


Check File

theory Check imports Submission begin


Terms and Conditions