From 3eacc374357bc2714bfeb8d397cfa73eda0d73b9 Mon Sep 17 00:00:00 2001 From: Francesco Protopapa Date: Mon, 9 Sep 2024 14:05:21 +0200 Subject: [PATCH] Fix introduction --- chapters/1-Introduction.typ | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/chapters/1-Introduction.typ b/chapters/1-Introduction.typ index 88fe4e0..b988a0c 100644 --- a/chapters/1-Introduction.typ +++ b/chapters/1-Introduction.typ @@ -19,7 +19,7 @@ This work demonstrates how controlling aliasing through an annotation system can In order to verify to Kotlin with Viper, it is necessary to translate the former language into the latter. However, this translation presents challenges due to fundamental differences between the two languages. Specifically, Viper's memory model is based on separation logic, which disallows shared mutable references. In contrast, Kotlin does not restrict aliasing, meaning that references in Kotlin can be both shared and mutable, posing a significant challenge when trying to encode Kotlin code into Viper. -This issue is clearly illustrated in the Kotlin code example provided in @intro-comp. In that example, the language allows the same reference to be passed multiple times when calling function `f`, thereby creating aliasing. @intro-comp also shows a wrong approach for encoding that Kotlin code into Viper. Despite the Viper code closely resembling the original Kotlin code, it fails verification when `f(x, x)` is called. This failure occurs because `f` requires write access to the field `n` of its arguments, but as previously mentioned, Viper’s separation logic disallows references from being both shared and mutable simultaneously. +This issue is clearly illustrated in the Kotlin code example provided in @intro-comp. In that example, the language allows the same reference to be passed multiple times when calling function `f`, thereby creating aliasing. Additionally, @intro-comp presents a naive approach for encoding that Kotlin code into Viper. Despite the Viper code closely resembling the original Kotlin code, it fails verification when `f(x, x)` is called. This failure occurs because `f` requires write access to the field `n` of its arguments, but as previously mentioned, Viper’s separation logic disallows references from being both shared and mutable simultaneously. #code-compare("Kotlin code with aliasing and its problematic encoding into Viper", .8fr, intro-kt, intro-vpr)