Re: Static code validation system for Lua

["Alexander Gladysh" <agladysh@...>]

On 1/8/07, Vyacheslav Egorov <mraleph@gorodok.net> wrote:
> Alexander Gladysh wrote:
> > But we've managed to
> > create a tool to validate game logic code, written by our
> > level-designers. Implemented validation system allowed us to catch
> > more errors early, and subjectively significantly sped up our
> > development process compared to projects, released before.
> Could you provide a more formal definition for "validation"? What are
> you validating?

Not sure about 'formal' stuff, but we were validating:

1. Those 'typos' -- everything which generates 'illegal' key access to
global (or other) environment; bad variable or function names. This
'minor' mistake can be a large PITA when is hidden in the dark corner
of the code, which is not covered by tests -- especially if global
table is not protected. Imagine:

function my_api_function() print "AHA!" end;
function end_user_code()
 my_api_funtion() -- Note the typo
end

The trivial mistake would not be found until end_user_code() would be
executed. Another example:

function another_function(my_variable)
 if my_vaiable > 0 then -- Due to typo, global variable is used here
   print "OK"
 else
   print "ERROR"
 end
end
another_function(5) -- Surprisingly, "ERROR" would be printed out

2. Also, we were validating API call arguments to the extent it is
possible to do statically. For example, we referenced objects of game
logic by string IDs. We had a static (relatively to application
run-time) lists of these IDs. We validated that API functions were
called with correct ID type:

local o = current_location:get_object_by_name("obj_chair") -- Correct?
local l = world:get_location_by_name("obj_chair") -- Wrong!

This protected us from typos, and from mistakes caused by object renaming.

To my experience, these two kinds of errors are quite common in
end-user code, and they significantly slow down development process
when not caught early.

> P.S. Some thoughts about static validation... I think level-designers
> usually do not use (don't need) a lot of Lua features.

This is exactly what I'm talking about. Lua is a great language, it
allows writing sophisticated expert-level programs efficiently, and,
in the same time, it allows inexperienced programmers to efficiently
code in-game logic without spending too much to learn complicated
programming stuff.

> So we are speaking here about verification of small Lua-subset (we need to throw
> away some features to reduce "dynamism" to make language more
> predictable... For example think about coroutines, we need to define
> here some kind of yield-points otherwise our reasoning system will be to
> conservative, and it'll be unable to decide anything...).

We simply had coroutine.* table not visible for end-user code. All
coroutine-based state machines the end-users needed to program, were
efficiently hidden behind callback interfaces.

> It is very interesting problem... Is it possible to build some kind of Hoare-logic
> for Lua?

Well, if it is possible at all for dynamic languages like Lua...
Anyway, I think this would be a large project for someone from
theoretical side -- my proposal is more from practical one :)

With best regards,
Alexander.