This topic contains 7 replies, has 1 voice, and was last updated by 
josh December 17, 2021 at 5:01 pm.
-
Posts
-
joshTo further clarify:
Say we have
I Metaprogramming/template libraries that can be instantiated as triples of Concrete Code x Unit Tests/Asserts x Proofs (proofs may be empty or some interesting theorems).
II. A concrete software versioned artifact that maps between NLP texts and instantiations of I at the level of saying whether or not the mapping is “consistent” and “faithful” – these properties are analogous to satisfiable & complete but they are colloquial rather than strict. The NLP software is making a best AI effort to say whether the intentions of consistent & faithful are met by the precise, concrete instantiation. The performance has been tested against opinions of human experts in substantive samples. The cautious natural writer/speaker can keep adding more text/dialog to gain greater assurance. Other tools permit asking for examples & counterexamples in particular cases of interest.
-
joshGood suggestion from the literature: real software functions typically allow several different code paths. Hoare logic type pattern statements are more useful & flexible if they compose over sets of possible code paths.
For software engineering, we typically want to sort claims/issues into aspects, some dealing with function semantics & some with performance or resource issues or name space usage or….
The ideal solution allows transformatins by editing – e.g. some extra task is to be accomplished on some of the code paths, while preserving the aspects & resource conservation targets that need to be preserved.
-
joshI find myself thinking about structured forms/context menus, labeled diagrams, etc as intermediaries between the code triples (I above) and NL. The properties of this land are:
a) unambiguous in terms of partial software spec but – the diagrams do not complete a Turing design. That’s left to the IDE. They may have versions of libraries & things that they ask for.
b) possibly unsatisfiable – they can represent a hope for a program that is not achievable or turns out to be inconsistent due to a IDE bug.
c) are readable & interpretable by trained generalists
d) easy to edit, and easy for humans to relate to NL sentences
e) various forms can be proposed in Q&A to help refine & disambiguate what the NL user is requesting.
-
joshThere could be a deeper technical language for writing new types of structured design forms at the intermediate level. A deep semantic description of both software & execution environments could conceivably support a language grounded in abstract machine & abstract code. Allowing definitions in terms of software tests & generational factories is easier & quicker. So assuming the plan is only to implement inverse mappings for software that’s part of the code system (no claim about automating complete understanding of 3rd party source), then the additional step to do the same for the abstract machine/code language is also a lot easier for the same reasons.
-
joshRegarding general code – claims of [I think it does THIS] are not as strong as [It’s been unit testing against THIS LIST OF CONDITIONS & RELATIONSHIPS] which is arguably less strong than a proof of a set of claims that subsumes all of the tests (rare). So building frameworks that include the both the unit testing & sophisticated ways of talking about that in pattern language is advancing the current state of the practical software arts.
-
joshAbility to use CASE tool analysis to generate unit tests in patterns can support testing that determines functionally correct patterns were observed on all executable paths that yield a functional result. This provides a higher level of correctness assurance.
-
joshIt may be efficient to define analysis modules as boundaries where range values of inputs, machine states, etc. are actually checked. And within analysis modules, mapping of analysis variable names to program variable names persist. Other conveniences like that so that sets of “basic conditions” can be defined & not restated for every function to be analyzed & test rigged.
-
-
-
-
You must be logged in to reply to this topic.