Automated Semantic Analysis of Formal Specifications
{'Code': '05010500', 'Directorate': {'Abbreviation': 'CSE', 'LongName': 'Direct For Computer & Info Scie & Enginr'}, 'Division': {'Abbreviation': 'CCF', 'LongName': 'Division of Computing and Communication Foundations'}}
{'SignBlockName': 'Janet L. Gatton', 'PO_EMAI': None, 'PO_PHON': None}
There is now widespread agreement that precise specifications can play          an important role in software development and maintenance.  It is less          clear that formal specification, as opposed to precise informal                 specifications, are worth the extra effort required to create them.             Proponents of formal specifications have argued that their                      susceptibility to machine analysis and manipulation increases their             value and reduces their cost.  This project is trying to support this           claim by building and using tools that aid in the construction of formal        specifications for programs and program modules.                                                                                                                The specification languages that have been used permit significant              assertions about logical properties of specifications--properties               related to consistency, completeness, and module independence--to be            made. Experience in hand checking specifications has lead to the                conviction that such assertions are useful in establishing the validity         of a specification.  Unfortunately, these assertions cannot be checked          completely by machine because they are all undecidable in the general           case.  Hence, this project will:                                                                                                                                    do the theoretical work necessary to design  useful approximations              to these checks;                                                                                                                                                implement a specification system that incorporates these                        approximations, building upon an existing syntax-directed editor and            term-rewriting laboratory;                                                                                                                                      evaluate these tools by using them to write specifications; and                 report on this experience, paying particular attention to the merits            of formal vs. precise informal, and definitional vs. operational,               specifications.
[{'FirstName': 'Stephen', 'LastName': 'Garland', 'PI_MID_INIT': 'J', 'PI_SUFX_NAME': None, 'PI_FULL_NAME': 'Stephen J Garland', 'EmailAddress': 'garland@lcs.mit.edu', 'NSF_ID': '000164743', 'StartDate': '07/01/1987', 'EndDate': None, 'RoleCode': 'Co-Principal Investigator'}, {'FirstName': 'John', 'LastName': 'Guttag', 'PI_MID_INIT': None, 'PI_SUFX_NAME': None, 'PI_FULL_NAME': 'John Guttag', 'EmailAddress': 'guttag@mit.edu', 'NSF_ID': '000184601', 'StartDate': '07/01/1987', 'EndDate': None, 'RoleCode': 'Principal Investigator'}]
{'Name': 'Massachusetts Institute of Technology', 'CityName': 'Cambridge', 'CountyName': 'MIDDLESEX', 'ZipCode': '021394301', 'PhoneNumber': '6172531000', 'StreetAddress': '77 MASSACHUSETTS AVE', 'StreetAddress2': 'NE18-901', 'CountryName': 'United States', 'StateName': 'Massachusetts', 'StateCode': 'MA', 'CONGRESSDISTRICT': '07', 'CONGRESS_DISTRICT_ORG': 'MA07', 'ORG_DUNS_NUM': '001425594', 'ORG_LGL_BUS_NAME': 'MASSACHUSETTS INSTITUTE OF TECHNOLOGY', 'ORG_PRNT_DUNS_NUM': '001425594'}
{'Name': None, 'CityName': None, 'CountyName': None, 'StateCode': None, 'ZipCode': None, 'StreetAddress': None, 'CountryCode': None, 'CountryName': None, 'StateName': None, 'CountryFlag': None, 'CONGRESSDISTRICT': None, 'CONGRESS_DISTRICT_PERF': '""'}
{'Code': '2880', 'Text': 'SOFTWARE ENGINEERING AND LANGU'}
{'url': 'https://www.nsf.gov/awardsearch/download?DownloadFileName=1987&All=true', 'xml': '8706652.xml'}