K-user mailing list

[Traian Florin Șerbănuță <traian.serbanuta AT info.uaic.ro>]

Hi Soha,

It's good to hear from you!

Radu and Michael, could you please shed some light in these matters?  They seem mostly related to parsing, and it is conceivable that they should work as Soha suggests.

2013/10/26 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.?

I think that should be possible and the fact you cannot do it means it's a bug we should look into.  

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.? 

I think that, again, this could be made to work, although, again,  you might need to  pass more options to kompile and krun.

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

We are in the process of redesigning Maps (and sets, bags, lists) to be more closely integrated with K, similarly to Integers and other builtin types.

In the meanwhile, one cannot subsort Maps to K and there might be some issues with mixing maps with concrete syntax, although I think this was already used in several projects, so there should be ways to circumvent this limitation.

The main issue is/was that it increases the number of ambiguities at parsing time.

best wishes,

Traian 

 

Thank you,

Soha

_______________________________________________
k-user mailing list
k-user AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/k-user