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.

## Resources

### 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

end```

### 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"

end```

### Check File

```theory Check imports Submission begin

end```

Terms and Conditions