From 9b3fe8993edda7a4bb79f6c8530a7ca77030d7f9 Mon Sep 17 00:00:00 2001 From: drganam Date: Mon, 21 Aug 2023 10:30:05 +0200 Subject: [PATCH 1/2] typo? --- core/src/sphinx/faq.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/core/src/sphinx/faq.rst b/core/src/sphinx/faq.rst index d61e6bdc8c..c80f0acb18 100644 --- a/core/src/sphinx/faq.rst +++ b/core/src/sphinx/faq.rst @@ -55,7 +55,7 @@ It is best to deploy formal verification when starting to develop software. In t Can I use Stainless with Java? ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -Scala has excellent interoperability with Java, so external libraries can be used to build application where some parts are verified using Stainless. Stainless uses Scala syntax trees and does not support verification of Java itself. Whereas functional Scala works as a both specification and implementation language, Java does appear to be a good language for specifications, so much that Java verification tools in the past introduced their own logical notation that developers then must learn in addition to Java. +Scala has excellent interoperability with Java, so external libraries can be used to build application where some parts are verified using Stainless. Stainless uses Scala syntax trees and does not support verification of Java itself. Whereas functional Scala works as a both specification and implementation language, Java does not appear to be a good language for specifications, so much that Java verification tools in the past introduced their own logical notation that developers then must learn in addition to Java. Can I use Stainless with Rust? ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ From 9fa109ae9e547ea818c57e7d728bed5ca96957c3 Mon Sep 17 00:00:00 2001 From: Dragana Date: Sun, 11 Feb 2024 14:11:36 +0100 Subject: [PATCH 2/2] equivalence is not transitive when there are requires --- .../main/scala/stainless/equivchk/EquivalenceChecker.scala | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/core/src/main/scala/stainless/equivchk/EquivalenceChecker.scala b/core/src/main/scala/stainless/equivchk/EquivalenceChecker.scala index 2b612ad7ae..5bee6c428e 100644 --- a/core/src/main/scala/stainless/equivchk/EquivalenceChecker.scala +++ b/core/src/main/scala/stainless/equivchk/EquivalenceChecker.scala @@ -566,6 +566,7 @@ class EquivalenceChecker(override val trees: Trees, val newParamTps = eqLemma0.tparams.map { tparam => tparam.tp } val newParamVars = eqLemma0.params.map { param => param.toVariable } + val specsModel = if conf.topLevel then symbols.functions(allModels.head) else conf.model val subst = { val nweParamVarsPermuted = conf.strat.order match { case EquivCheckOrder.ModelFirst => @@ -575,12 +576,12 @@ class EquivalenceChecker(override val trees: Trees, // f1 = candidate, f2 = model: we need to "undo" the ordering perm.m2c.map(newParamVars) } - (conf.model.params.map(_.id) zip nweParamVarsPermuted).toMap + (specsModel.params.map(_.id) zip nweParamVarsPermuted).toMap } - val tsubst = (conf.model.tparams zip newParamTps).map { case (tparam, targ) => tparam.tp.id -> targ }.toMap + val tsubst = (specsModel.tparams zip newParamTps).map { case (tparam, targ) => tparam.tp.id -> targ }.toMap val specializer = new Specializer(eqLemma0, eqLemma0.id, tsubst, subst, Map()) - val specs = BodyWithSpecs(conf.model.fullBody).specs.filter(s => s.kind == LetKind || s.kind == PreconditionKind) + val specs = BodyWithSpecs(specsModel.fullBody).specs.filter(s => s.kind == LetKind || s.kind == PreconditionKind) val pre = specs.map { case Precondition(cond) => Precondition(specializer.transform(cond)) case LetInSpec(vd, expr) => LetInSpec(vd, specializer.transform(expr))