K-user mailing list

[Dwight Guth <dwight.guth AT runtimeverification.com>]

Hi,

If you use the _Map_ klabel to concatenate two maps together, and they contain keys that have different values, this is an error. Users who want to combine maps in this fashion should specify which map overwrites the value of the other when keys are shared by using the updateMap klabel.

The ! operator is guaranteed only to be unique within the domain of other identifiers obtained via !. In practice, it will generate the sequence _0, _1, _2, ... You can change this behavior if you wish by defining your own portion of the prelude corresponding to identifiers. The two sentences in the prelude corresponding to the fresh generation of objects of sort Id are in the ID module and are as follows:

syntax Id ::= freshId(Int) [freshGenerator, function]
rule freshId(I:Int) => String2Id("_" +String Int2String(I))

You can simply change the second rule to generate any syntax for fresh identifiers you wish, making use of the fresh counter (the integer variable) to ensure uniqueness across all fresh identifiers.

On Sun, May 1, 2016 at 7:09 PM, Eric Huber <echuber2 AT illinois.edu> wrote:

Hi, I am just wondering what exactly happens when you concatenate K
Map built-ins. It seems that concatenating a new mapping to an
existing Map hides any existing mapping with the same key, but does it
make a difference if the concatenation is done with the "new" mapping
on the left or right of the other Map?

Also, when the "!" operator is used to generate an identifier with
freshness constraints, what determines the range of identifiers for
which the freshness is guaranteed?

Thanks,
Eric Huber