K-user mailing list

[soha hussein <husseinsoh AT gmail.com>]

Hi,

I am Soha Hussein, I used to work in the JavaMOP team. Currently i'm working in Carnegie Mellon Qatar, and we are working on inferring some program features by typing for the purpose of enforcing some security properties. We used to work with Twelf, but Twelf has some limitations that doesn't allow us to manipulate the context of variables easily while typing. I suggested using K, and actually i've implemented our old language in it already and it is working pretty well. They liked it and now i'm in the step of adding more on our old typing system, I generally manipulate the maps which contains the context, 

I have two questions,

1. I want to populate the configuration while running, so i created the configuration variable $SRV and called krun with the -cSRV option. It works as long as I am not using something of sort Id. In fact i tried to run lambda_1 lesson_6 k program with the -cPGM option and the example in the reference manual  "-cPGM="lambda x . x", but again it complaining from x, if i tried to run , "1 + 1" it works fine. So the question is what is the problem with variables of sort Id.? How can i populate the configuration of things that has sort Id.?

2. My second question is about maps, if i tried to have something like that

syntax Exp ::= "{" Map"}", when i try to have a program that contains a map of this form, it doesn't compile. To go around this, i implement a List and then convert the List input into the Map, but this seems unnecessary and thought may be there is something better to do there.? 

Also I would appreciate if you gave me more information on Maps as well as their limitations.

Thank you,

Soha